This is an automated email from the git hooks/post-receive script. treinen pushed a change to branch upstream in repository alt-ergo.
from 5dc7ee9 Imported Upstream version 0.95.2 adds da20a0b Imported Upstream version 0.99.1+dfsg1 No new revisions were added by this update. Summary of changes: CHANGES | 32 ++ COPYING | 25 -- COPYING.md | 28 ++ INSTALL | 32 -- INSTALL.md | 74 ++++ Makefile | 3 + Makefile.configurable.in | 58 +++ Makefile.in | 485 ---------------------- Makefile.users | 334 +++++++++++++++ README.md | 52 +-- configure | 238 +++++------ configure.in | 12 +- doc/ergoheader.txt | 16 - doc/headache_config.txt | 14 - src/gui/gui_replay.ml | 12 +- src/gui/gui_replay.mli | 6 + src/gui/gui_session.ml | 6 + src/gui/gui_session.mli | 6 + src/gui/why_annoted.ml | 35 +- src/gui/why_annoted.mli | 8 +- src/gui/why_connected.ml | 46 ++- src/gui/why_connected.mli | 8 +- src/instances/matching.ml | 451 ++++++++++++++------ src/instances/matching.mli | 66 ++- src/main/frontend.ml | 374 ++++++++--------- src/main/frontend.mli | 35 +- src/main/main_gui.ml | 62 ++- src/main/main_gui.mli | 6 + src/main/main_text.ml | 42 +- src/main/main_text.mli | 6 + src/parsing/errors.ml | 6 + src/parsing/errors.mli | 6 + src/parsing/smt_lex.mll | 6 + src/parsing/smt_parser.mly | 6 + src/parsing/smtlib2_lex.mll | 6 + src/parsing/smtlib2_parse.mly | 6 + src/parsing/why_lexer.mll | 18 - src/parsing/why_parser.mly | 60 +-- src/preprocess/cnf.ml | 206 +--------- src/preprocess/cnf.mli | 13 +- src/preprocess/existantial.ml | 6 + src/preprocess/existantial.mli | 6 + src/preprocess/pruning.ml | 20 +- src/preprocess/pruning.mli | 6 + src/preprocess/smt_to_why.ml | 22 +- src/preprocess/smtlib2_to_why.ml | 12 +- src/preprocess/triggers.ml | 11 +- src/preprocess/triggers.mli | 6 + src/preprocess/why_typing.ml | 26 +- src/preprocess/why_typing.mli | 6 + src/sat/sat.ml | 654 ----------------------------- src/sat/sat.mli | 52 --- src/sat/sat_solvers.ml | 591 +++++++++++++++++++++++++++ src/sat/sat_solvers.mli | 65 +++ src/structures/exception.ml | 6 + src/structures/exception.mli | 6 + src/structures/explanation.ml | 131 +++--- src/structures/explanation.mli | 44 +- src/structures/formula.ml | 70 +++- src/structures/formula.mli | 18 + src/structures/literal.ml | 230 ++++++++--- src/structures/literal.mli | 36 +- src/structures/smt_ast.mli | 6 + src/structures/smtlib2_ast.ml | 6 + src/structures/smtlib2_ast.mli | 6 + src/structures/subst.ml | 46 --- src/structures/subst.mli | 34 -- src/structures/symbols.ml | 6 + src/structures/symbols.mli | 6 + src/structures/term.ml | 17 + src/structures/term.mli | 21 +- src/structures/ty.ml | 10 +- src/structures/ty.mli | 6 + src/structures/why_ptree.ml | 14 +- src/structures/why_ptree.mli | 14 +- src/theories/ac.ml | 61 +-- src/theories/ac.mli | 6 + src/theories/arith.ml | 130 +++--- src/theories/arith.mli | 24 +- src/theories/arrays.ml | 716 ++++++++++++++++---------------- src/theories/arrays.mli | 15 +- src/theories/bitv.ml | 38 +- src/theories/bitv.mli | 14 +- src/theories/boxed.ml | 65 --- src/theories/boxed.mli | 42 -- src/theories/cc.ml | 726 --------------------------------- src/theories/combine.ml | 398 +++++++++++------- src/theories/combine.mli | 14 +- src/theories/custom_theory.ml | 486 ---------------------- src/theories/custom_theory.mli | 31 -- src/theories/fm.ml | 205 +++++----- src/theories/fm.mli | 16 +- src/theories/incr_match.ml | 390 ------------------ src/theories/incr_match.mli | 37 -- src/theories/instantiation.ml | 468 --------------------- src/theories/instantiation.mli | 53 --- src/theories/intervals.ml | 8 +- src/theories/intervals.mli | 6 + src/theories/polynome.ml | 8 +- src/theories/polynome.mli | 6 + src/theories/records.ml | 67 +-- src/theories/records.mli | 13 +- src/theories/sig.mli | 97 +---- src/theories/sum.ml | 446 ++++++++++---------- src/theories/sum.mli | 13 +- src/theories/theory.ml | 793 ++++++++++++++++++++++++++++++++++++ src/theories/{cc.mli => theory.mli} | 16 +- src/theories/uf.ml | 331 +++++++-------- src/theories/uf.mli | 27 +- src/theories/use.ml | 96 ++--- src/theories/use.mli | 30 +- src/util/hashcons.ml | 16 - src/util/hashcons.mli | 61 +-- src/util/hstring.ml | 6 + src/util/hstring.mli | 6 + src/util/loc.ml | 6 + src/util/loc.mli | 6 + src/util/numbers.ml | 28 +- src/util/numbers.mli | 6 + src/util/options.ml | 94 +++-- src/util/options.mli | 30 +- src/util/timers.ml | 6 + src/util/timers.mli | 6 + src/util/version.ml | 3 + src/util/version.mli | 17 +- 125 files changed, 5161 insertions(+), 6143 deletions(-) delete mode 100644 COPYING create mode 100644 COPYING.md delete mode 100644 INSTALL create mode 100644 INSTALL.md create mode 100644 Makefile create mode 100644 Makefile.configurable.in delete mode 100644 Makefile.in create mode 100644 Makefile.users delete mode 100644 doc/ergoheader.txt delete mode 100644 doc/headache_config.txt delete mode 100644 src/sat/sat.ml delete mode 100644 src/sat/sat.mli create mode 100644 src/sat/sat_solvers.ml create mode 100644 src/sat/sat_solvers.mli delete mode 100644 src/structures/subst.ml delete mode 100644 src/structures/subst.mli delete mode 100644 src/theories/boxed.ml delete mode 100644 src/theories/boxed.mli delete mode 100644 src/theories/cc.ml delete mode 100644 src/theories/custom_theory.ml delete mode 100644 src/theories/custom_theory.mli delete mode 100644 src/theories/incr_match.ml delete mode 100644 src/theories/incr_match.mli delete mode 100644 src/theories/instantiation.ml delete mode 100644 src/theories/instantiation.mli create mode 100644 src/theories/theory.ml rename src/theories/{cc.mli => theory.mli} (75%) create mode 100644 src/util/version.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