This is an automated email from the git hooks/post-receive script.

treinen pushed a change to branch experimental/master
in repository alt-ergo.

      from  93ae5f0   upload to experimental
      adds  231d305   upload to sid
      adds  4cb6613   lib-dev package breaks/replaces alt-ergo in versions 
before package split
      adds  4363a13   debian/watch : new site @ ocamlpro
      adds  5dc7ee9   Imported Upstream version 0.95.2
      adds  51132e0   Merge tag 'upstream/0.95.2'
      adds  99bea10   refresh patch 0001-No-need-to-activate-debug-flag.patch
      adds  c2476f3   drop patch 
0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
      adds  fbd9f75   drop patch 0003-Fix-a-typo.patch
      adds  eeac213   drop patch 0004-Add-rules-and-targets-for-gui.byte.patch
      adds  368bca3   drop patch 
0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
      adds  996dbd0   drop patch 0007-Fix-all-target.patch
      adds  dca871a   drop patch 0009-clean-remove-META.patch
      adds  ba352a9   + build-dep on libzarith-ocaml-dev
      adds  ee16ced   debian/rules : drop backup of .depends
      adds  e6907cc   debian/rules : additional make targets for build and 
install
      adds  f920a24   drop mandir setting in invocation of ./configure
      adds  15e39bf   debian/rules: drop touching of configure
      adds  18bc16a   + changelog entry: new upstream release
      adds  b5daf76   fix filenamemangle in debian/watch
      adds  0413dbd   update debian/copyright
      adds  5dff4ab   install examples
      adds  8524fde   drop overwrite of dh_auto_configure
      adds  2ca15d4   standards-version 3.9.5
      adds  a0fbd4f   add todo
      adds  a257ccf   Port to OCamlgraph 1.8.4 (Closes: #743072)
      adds  088a28a   Release to unstable
      adds  7d41a30   Revert "Port to OCamlgraph 1.8.4 (Closes: #743072)"
      adds  f184ab2   Revert back to match OCamlgraph 1.8.5 API.
      adds  5fd8c71   Release to unstable
       new  f4be06c   debian/copyright : Files-Excluded: non-free
       new  da20a0b   Imported Upstream version 0.99.1+dfsg1
       new  1816bce   Merge tag 'upstream/0.99.1+dfsg1' into experimental/master
       new  d12791c   new upstream 0.99.1
       new  476fbac   debian/rules clean target : execute ony when 
config.status exists
       new  adafe15   update patch 0001-No-need-to-activate-debug-flag
       new  adf7037   fix Makefile.users for dropping of non-free dirfectory
       new  3ae0b13   debian/rules : drop install-pack
       new  14ee89e   drop libalt-ergo-ocaml-dev binary package
       new  e61f1c9   bump standards-version
       new  5f1b37b   debian/watch : mangle +dfsg\d* \version suffix

The 11 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 .depend                                            |  263 ----
 CHANGES                                            |   43 +
 COPYING                                            |   12 -
 COPYING.md                                         |   28 +
 INSTALL                                            |   35 -
 INSTALL.md                                         |   74 ++
 CeCILL-C => LICENSE                                |    0
 Makefile                                           |    3 +
 Makefile.configurable.in                           |   58 +
 Makefile.in                                        |  418 ------
 Makefile.users                                     |  334 +++++
 README                                             |   36 -
 README.md                                          |   22 +
 arith.ml                                           |  592 ---------
 arith.mli                                          |   26 -
 arrays.ml                                          |  439 -------
 boxed.ml                                           |   68 -
 boxed.mli                                          |   45 -
 cc.ml                                              |  719 ----------
 cnf.ml                                             |  422 ------
 cnf.mli                                            |   29 -
 combine.mli                                        |   20 -
 common.ml                                          |  257 ----
 configure                                          |  318 +++--
 configure.in                                       |   74 +-
 custom_theory.ml                                   |  485 -------
 custom_theory.mli                                  |   34 -
 debian/alt-ergo.examples                           |    1 +
 debian/changelog                                   |   78 ++
 debian/control                                     |   24 +-
 debian/copyright                                   |   19 +-
 debian/libalt-ergo-ocaml-dev.install               |    1 -
 .../0001-No-need-to-activate-debug-flag.patch      |   20 +-
 ...the-test-if-test.mlw-is-absent-and-use-be.patch |   24 -
 debian/patches/0002-non-free-dropped               |   35 +
 debian/patches/0003-Fix-a-typo.patch               |   16 -
 .../0004-Add-rules-and-targets-for-gui.byte.patch  |   72 -
 ...ma-instead-of-cmxa-for-lablgtksourceview2.patch |   42 -
 debian/patches/0007-Fix-all-target.patch           |   26 -
 ...ll-pack-into-two-separate-targets-opt-and.patch |   33 -
 debian/patches/0009-clean-remove-META.patch        |   17 -
 debian/patches/series                              |    8 +-
 debian/rules                                       |   25 +-
 debian/todo                                        |    2 +
 debian/watch                                       |    3 +-
 {util => doc}/gtk-lang/alt-ergo.lang               |    0
 examples/invalid/arith1.why                        |    5 +
 examples/invalid/arith2.why                        |    4 +
 examples/invalid/arrays.why                        |   12 +
 examples/invalid/bitv.why                          |    7 +
 examples/valid/ac_arith.why                        |    3 +
 examples/valid/arith1.why                          |    9 +
 examples/valid/arith2.why                          |   10 +
 examples/valid/arith3.why                          |    7 +
 examples/valid/arith4.why                          |    2 +
 examples/valid/arrays.why                          |   12 +
 examples/valid/bitv.why                            |    5 +
 examples/valid/congruence.why                      |   10 +
 examples/valid/enum_arrays.why                     |   11 +
 examples/valid/quantifiers.why                     |   14 +
 explanation.ml                                     |  155 ---
 fm.ml                                              | 1011 --------------
 frontend.ml                                        |  260 ----
 frontend.mli                                       |   53 -
 gui_replay.mli                                     |    4 -
 hashcons.mli                                       |  129 --
 incr_match.ml                                      |  393 ------
 incr_match.mli                                     |   39 -
 instantiation.ml                                   |  470 -------
 instantiation.mli                                  |   54 -
 literal.ml                                         |  236 ----
 matching.ml                                        |  341 -----
 matching.mli                                       |   61 -
 options.ml                                         |  150 ---
 parseoptions.ml                                    |  124 --
 preoptions.ml                                      |  116 --
 preoptions.mli                                     |   96 --
 pretty.ml                                          |   66 -
 pretty.mli                                         |   25 -
 print_color.ml                                     |  208 ---
 print_color.mli                                    |  102 --
 pruning.ml                                         |  370 ------
 revision.sh                                        |   31 -
 sat.ml                                             |  636 ---------
 sat.mli                                            |   55 -
 sig.mli                                            |  238 ----
 smt_to_why.ml                                      |  273 ----
 smtlib2_util.ml                                    |   31 -
 src/Makefile                                       |    9 +
 src/gui/Makefile                                   |    9 +
 gui_replay.ml => src/gui/gui_replay.ml             |   30 +-
 arrays.mli => src/gui/gui_replay.mli               |   52 +-
 gui_session.ml => src/gui/gui_session.ml           |   39 +-
 gui_session.mli => src/gui/gui_session.mli         |   39 +-
 why_annoted.ml => src/gui/why_annoted.ml           |  927 +++++++------
 why_annoted.mli => src/gui/why_annoted.mli         |   53 +-
 why_connected.ml => src/gui/why_connected.ml       |  750 +++++------
 why_connected.mli => src/gui/why_connected.mli     |   41 +-
 src/instances/Makefile                             |    9 +
 src/instances/matching.ml                          |  604 +++++++++
 src/instances/matching.mli                         |   51 +
 src/main/Makefile                                  |    9 +
 src/main/frontend.ml                               |  237 ++++
 src/main/frontend.mli                              |   54 +
 gui.ml => src/main/main_gui.ml                     |  987 +++++++-------
 arrays.mli => src/main/main_gui.mli                |   51 +-
 src/main/main_text.ml                              |   77 ++
 bitv.mli => src/main/main_text.mli                 |   50 +-
 src/parsing/Makefile                               |    9 +
 src/parsing/errors.ml                              |  143 ++
 common.mli => src/parsing/errors.mli               |   63 +-
 smt_lex.mll => src/parsing/smt_lex.mll             |   39 +-
 smt_parser.mly => src/parsing/smt_parser.mly       |   39 +-
 smtlib2_lex.mll => src/parsing/smtlib2_lex.mll     |   44 +-
 smtlib2_parse.mly => src/parsing/smtlib2_parse.mly |   39 +-
 why_lexer.mll => src/parsing/why_lexer.mll         |   65 +-
 why_parser.mly => src/parsing/why_parser.mly       |  190 ++-
 src/preprocess/Makefile                            |    9 +
 src/preprocess/cnf.ml                              |  258 ++++
 main.ml => src/preprocess/cnf.mli                  |   52 +-
 existantial.ml => src/preprocess/existantial.ml    |   67 +-
 existantial.mli => src/preprocess/existantial.mli  |   39 +-
 src/preprocess/pruning.ml                          |  375 ++++++
 pruning.mli => src/preprocess/pruning.mli          |   39 +-
 src/preprocess/smt_to_why.ml                       |  276 ++++
 .../preprocess/smtlib2_to_why.ml                   |  118 +-
 triggers.ml => src/preprocess/triggers.ml          |  719 +++++-----
 triggers.mli => src/preprocess/triggers.mli        |   40 +-
 src/preprocess/why_typing.ml                       | 1380 +++++++++++++++++++
 why_typing.mli => src/preprocess/why_typing.mli    |   39 +-
 src/sat/Makefile                                   |    9 +
 src/sat/sat_solvers.ml                             |  591 +++++++++
 src/sat/sat_solvers.mli                            |   65 +
 src/structures/Makefile                            |    9 +
 exception.ml => src/structures/exception.ml        |   39 +-
 exception.mli => src/structures/exception.mli      |   39 +-
 src/structures/explanation.ml                      |  147 +++
 explanation.mli => src/structures/explanation.mli  |   79 +-
 formula.ml => src/structures/formula.ml            |  391 +++---
 formula.mli => src/structures/formula.mli          |   51 +-
 src/structures/literal.ml                          |  335 +++++
 literal.mli => src/structures/literal.mli          |   73 +-
 smt_ast.mli => src/structures/smt_ast.mli          |   51 +-
 smtlib2_ast.ml => src/structures/smtlib2_ast.ml    |   45 +-
 src/structures/smtlib2_ast.mli                     |  131 ++
 symbols.ml => src/structures/symbols.ml            |   54 +-
 symbols.mli => src/structures/symbols.mli          |   43 +-
 term.ml => src/structures/term.ml                  |  161 ++-
 term.mli => src/structures/term.mli                |   56 +-
 ty.ml => src/structures/ty.ml                      |  301 ++---
 ty.mli => src/structures/ty.mli                    |   61 +-
 why_ptree.mli => src/structures/why_ptree.ml       |  155 ++-
 why_ptree.mli => src/structures/why_ptree.mli      |   64 +-
 src/theories/Makefile                              |    9 +
 ac.ml => src/theories/ac.ml                        |  190 +--
 ac.mli => src/theories/ac.mli                      |   38 +-
 src/theories/arith.ml                              |  548 ++++++++
 src/theories/arith.mli                             |   41 +
 src/theories/arrays.ml                             |  442 +++++++
 arrays.mli => src/theories/arrays.mli              |   46 +-
 bitv.ml => src/theories/bitv.ml                    |  563 ++++----
 bitv.mli => src/theories/bitv.mli                  |   47 +-
 combine.ml => src/theories/combine.ml              |  505 ++++---
 src/theories/combine.mli                           |   29 +
 src/theories/fm.ml                                 | 1051 +++++++++++++++
 fm.mli => src/theories/fm.mli                      |   49 +-
 intervals.ml => src/theories/intervals.ml          |  431 +++---
 intervals.mli => src/theories/intervals.mli        |   56 +-
 polynome.ml => src/theories/polynome.ml            |  264 ++--
 polynome.mli => src/theories/polynome.mli          |   68 +-
 records.ml => src/theories/records.ml              |  286 ++--
 records.mli => src/theories/records.mli            |   46 +-
 src/theories/sig.mli                               |  136 ++
 src/theories/sum.ml                                |  392 ++++++
 sum.mli => src/theories/sum.mli                    |   46 +-
 src/theories/theory.ml                             |  793 +++++++++++
 cc.mli => src/theories/theory.mli                  |   49 +-
 uf.ml => src/theories/uf.ml                        |  679 +++++-----
 uf.mli => src/theories/uf.mli                      |   61 +-
 src/theories/use.ml                                |  122 ++
 use.mli => src/theories/use.mli                    |   65 +-
 src/util/Makefile                                  |    9 +
 hashcons.ml => src/util/hashcons.ml                |   68 +-
 src/util/hashcons.mli                              |  109 ++
 hstring.ml => src/util/hstring.ml                  |   53 +-
 hstring.mli => src/util/hstring.mli                |   44 +-
 loc.ml => src/util/loc.ml                          |   45 +-
 arrays.mli => src/util/loc.mli                     |   51 +-
 src/util/numbers.ml                                |  165 +++
 src/util/numbers.mli                               |   69 +
 src/util/options.ml                                |  356 +++++
 options.mli => src/util/options.mli                |  229 ++--
 timers.ml => src/util/timers.ml                    |   43 +-
 timers.mli => src/util/timers.mli                  |   39 +-
 src/util/version.ml                                |    3 +
 src/util/version.mli                               |   10 +
 subst.ml                                           |   49 -
 subst.mli                                          |   37 -
 sum.ml                                             |  339 -----
 use.ml                                             |  124 --
 why_typing.ml                                      | 1390 --------------------
 201 files changed, 15520 insertions(+), 16972 deletions(-)
 delete mode 100644 .depend
 delete mode 100644 COPYING
 create mode 100644 COPYING.md
 delete mode 100644 INSTALL
 create mode 100644 INSTALL.md
 rename CeCILL-C => LICENSE (100%)
 create mode 100644 Makefile
 create mode 100644 Makefile.configurable.in
 delete mode 100644 Makefile.in
 create mode 100644 Makefile.users
 delete mode 100644 README
 create mode 100644 README.md
 delete mode 100644 arith.ml
 delete mode 100644 arith.mli
 delete mode 100644 arrays.ml
 delete mode 100644 boxed.ml
 delete mode 100644 boxed.mli
 delete mode 100644 cc.ml
 delete mode 100644 cnf.ml
 delete mode 100644 cnf.mli
 delete mode 100644 combine.mli
 delete mode 100644 common.ml
 delete mode 100644 custom_theory.ml
 delete mode 100644 custom_theory.mli
 create mode 100644 debian/alt-ergo.examples
 delete mode 100644 debian/libalt-ergo-ocaml-dev.install
 delete mode 100644 
debian/patches/0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
 create mode 100644 debian/patches/0002-non-free-dropped
 delete mode 100644 debian/patches/0003-Fix-a-typo.patch
 delete mode 100644 debian/patches/0004-Add-rules-and-targets-for-gui.byte.patch
 delete mode 100644 
debian/patches/0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
 delete mode 100644 debian/patches/0007-Fix-all-target.patch
 delete mode 100644 
debian/patches/0008-Split-install-pack-into-two-separate-targets-opt-and.patch
 delete mode 100644 debian/patches/0009-clean-remove-META.patch
 create mode 100644 debian/todo
 rename {util => doc}/gtk-lang/alt-ergo.lang (100%)
 create mode 100644 examples/invalid/arith1.why
 create mode 100644 examples/invalid/arith2.why
 create mode 100644 examples/invalid/arrays.why
 create mode 100644 examples/invalid/bitv.why
 create mode 100644 examples/valid/ac_arith.why
 create mode 100644 examples/valid/arith1.why
 create mode 100644 examples/valid/arith2.why
 create mode 100644 examples/valid/arith3.why
 create mode 100644 examples/valid/arith4.why
 create mode 100644 examples/valid/arrays.why
 create mode 100644 examples/valid/bitv.why
 create mode 100644 examples/valid/congruence.why
 create mode 100644 examples/valid/enum_arrays.why
 create mode 100644 examples/valid/quantifiers.why
 delete mode 100644 explanation.ml
 delete mode 100644 fm.ml
 delete mode 100644 frontend.ml
 delete mode 100644 frontend.mli
 delete mode 100644 gui_replay.mli
 delete mode 100644 hashcons.mli
 delete mode 100644 incr_match.ml
 delete mode 100644 incr_match.mli
 delete mode 100644 instantiation.ml
 delete mode 100644 instantiation.mli
 delete mode 100644 literal.ml
 delete mode 100644 matching.ml
 delete mode 100644 matching.mli
 delete mode 100644 options.ml
 delete mode 100644 parseoptions.ml
 delete mode 100644 preoptions.ml
 delete mode 100644 preoptions.mli
 delete mode 100644 pretty.ml
 delete mode 100644 pretty.mli
 delete mode 100644 print_color.ml
 delete mode 100644 print_color.mli
 delete mode 100644 pruning.ml
 delete mode 100755 revision.sh
 delete mode 100644 sat.ml
 delete mode 100644 sat.mli
 delete mode 100644 sig.mli
 delete mode 100644 smt_to_why.ml
 delete mode 100644 smtlib2_util.ml
 create mode 100644 src/Makefile
 create mode 100644 src/gui/Makefile
 rename gui_replay.ml => src/gui/gui_replay.ml (56%)
 copy arrays.mli => src/gui/gui_replay.mli (53%)
 rename gui_session.ml => src/gui/gui_session.ml (83%)
 rename gui_session.mli => src/gui/gui_session.mli (64%)
 rename why_annoted.ml => src/gui/why_annoted.ml (66%)
 rename why_annoted.mli => src/gui/why_annoted.mli (89%)
 rename why_connected.ml => src/gui/why_connected.ml (61%)
 rename why_connected.mli => src/gui/why_connected.mli (65%)
 create mode 100644 src/instances/Makefile
 create mode 100644 src/instances/matching.ml
 create mode 100644 src/instances/matching.mli
 create mode 100644 src/main/Makefile
 create mode 100644 src/main/frontend.ml
 create mode 100644 src/main/frontend.mli
 rename gui.ml => src/main/main_gui.ml (60%)
 copy arrays.mli => src/main/main_gui.mli (54%)
 create mode 100644 src/main/main_text.ml
 copy bitv.mli => src/main/main_text.mli (54%)
 create mode 100644 src/parsing/Makefile
 create mode 100644 src/parsing/errors.ml
 rename common.mli => src/parsing/errors.mli (62%)
 rename smt_lex.mll => src/parsing/smt_lex.mll (85%)
 rename smt_parser.mly => src/parsing/smt_parser.mly (90%)
 rename smtlib2_lex.mll => src/parsing/smtlib2_lex.mll (77%)
 rename smtlib2_parse.mly => src/parsing/smtlib2_parse.mly (92%)
 rename why_lexer.mll => src/parsing/why_lexer.mll (66%)
 rename why_parser.mly => src/parsing/why_parser.mly (56%)
 create mode 100644 src/preprocess/Makefile
 create mode 100644 src/preprocess/cnf.ml
 rename main.ml => src/preprocess/cnf.mli (53%)
 rename existantial.ml => src/preprocess/existantial.ml (73%)
 rename existantial.mli => src/preprocess/existantial.mli (56%)
 create mode 100644 src/preprocess/pruning.ml
 rename pruning.mli => src/preprocess/pruning.mli (58%)
 create mode 100644 src/preprocess/smt_to_why.ml
 rename smtlib2_to_why.ml => src/preprocess/smtlib2_to_why.ml (88%)
 rename triggers.ml => src/preprocess/triggers.ml (50%)
 rename triggers.mli => src/preprocess/triggers.mli (61%)
 create mode 100644 src/preprocess/why_typing.ml
 rename why_typing.mli => src/preprocess/why_typing.mli (63%)
 create mode 100644 src/sat/Makefile
 create mode 100644 src/sat/sat_solvers.ml
 create mode 100644 src/sat/sat_solvers.mli
 create mode 100644 src/structures/Makefile
 rename exception.ml => src/structures/exception.ml (59%)
 rename exception.mli => src/structures/exception.mli (59%)
 create mode 100644 src/structures/explanation.ml
 rename explanation.mli => src/structures/explanation.mli (56%)
 rename formula.ml => src/structures/formula.ml (58%)
 rename formula.mli => src/structures/formula.mli (74%)
 create mode 100644 src/structures/literal.ml
 rename literal.mli => src/structures/literal.mli (54%)
 rename smt_ast.mli => src/structures/smt_ast.mli (77%)
 rename smtlib2_ast.ml => src/structures/smtlib2_ast.ml (87%)
 create mode 100644 src/structures/smtlib2_ast.mli
 rename symbols.ml => src/structures/symbols.ml (78%)
 rename symbols.mli => src/structures/symbols.mli (69%)
 rename term.ml => src/structures/term.ml (64%)
 rename term.mli => src/structures/term.mli (64%)
 rename ty.ml => src/structures/ty.ml (61%)
 rename ty.mli => src/structures/ty.mli (69%)
 copy why_ptree.mli => src/structures/why_ptree.ml (59%)
 rename why_ptree.mli => src/structures/why_ptree.mli (83%)
 create mode 100644 src/theories/Makefile
 rename ac.ml => src/theories/ac.ml (61%)
 rename ac.mli => src/theories/ac.mli (74%)
 create mode 100644 src/theories/arith.ml
 create mode 100644 src/theories/arith.mli
 create mode 100644 src/theories/arrays.ml
 copy arrays.mli => src/theories/arrays.mli (53%)
 rename bitv.ml => src/theories/bitv.ml (63%)
 rename bitv.mli => src/theories/bitv.mli (53%)
 rename combine.ml => src/theories/combine.ml (58%)
 create mode 100644 src/theories/combine.mli
 create mode 100644 src/theories/fm.ml
 rename fm.mli => src/theories/fm.mli (54%)
 rename intervals.ml => src/theories/intervals.ml (66%)
 rename intervals.mli => src/theories/intervals.mli (54%)
 rename polynome.ml => src/theories/polynome.ml (50%)
 rename polynome.mli => src/theories/polynome.mli (60%)
 rename records.ml => src/theories/records.ml (65%)
 rename records.mli => src/theories/records.mli (53%)
 create mode 100644 src/theories/sig.mli
 create mode 100644 src/theories/sum.ml
 rename sum.mli => src/theories/sum.mli (53%)
 create mode 100644 src/theories/theory.ml
 rename cc.mli => src/theories/theory.mli (57%)
 rename uf.ml => src/theories/uf.ml (51%)
 rename uf.mli => src/theories/uf.mli (52%)
 create mode 100644 src/theories/use.ml
 rename use.mli => src/theories/use.mli (51%)
 create mode 100644 src/util/Makefile
 rename hashcons.ml => src/util/hashcons.ml (57%)
 create mode 100644 src/util/hashcons.mli
 rename hstring.ml => src/util/hstring.ml (55%)
 rename hstring.mli => src/util/hstring.mli (58%)
 rename loc.ml => src/util/loc.ml (54%)
 rename arrays.mli => src/util/loc.mli (51%)
 create mode 100644 src/util/numbers.ml
 create mode 100644 src/util/numbers.mli
 create mode 100644 src/util/options.ml
 rename options.mli => src/util/options.mli (56%)
 rename timers.ml => src/util/timers.ml (78%)
 rename timers.mli => src/util/timers.mli (63%)
 create mode 100644 src/util/version.ml
 create mode 100644 src/util/version.mli
 delete mode 100644 subst.ml
 delete mode 100644 subst.mli
 delete mode 100644 sum.ml
 delete mode 100644 use.ml
 delete mode 100644 why_typing.ml

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/alt-ergo.git

_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

Reply via email to