This is an automated email from the git hooks/post-receive script. treinen pushed a change to branch experimental/upstream in repository alt-ergo.
from e8667c8 Imported Upstream version 0.95.1 adds 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: .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 - {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 -------------------- 183 files changed, 15378 insertions(+), 16668 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 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