This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository alt-ergo.
commit 5fc61c24a4df9fb5dc57e587ea16ca805d4e36e5
Merge: c7774aa f60d17b
Author: Ralf Treinen <trei...@free.fr>
Date: Sun Feb 28 20:08:13 2016 +0100
Merge tag 'upstream/1.01'
Upstream version 1.01
CHANGES | 187 ++++
INSTALL.md | 40 +-
Makefile.configurable.in | 3 +-
Makefile.users | 119 ++-
README.md | 2 +-
configure | 89 +-
configure.in | 42 +-
src/Makefile | 9 -
src/gui/Makefile | 9 -
src/gui/gui_replay.ml | 16 +-
src/gui/gui_replay.mli | 2 +-
src/gui/gui_session.ml | 16 +-
src/gui/gui_session.mli | 2 +-
src/gui/why_annoted.ml | 317 +++---
src/gui/why_annoted.mli | 92 +-
src/gui/why_connected.ml | 186 ++--
src/gui/why_connected.mli | 6 +-
src/instances/Makefile | 9 -
src/instances/matching.ml | 537 ++++++----
src/instances/matching.mli | 7 +-
src/main/Makefile | 9 -
src/main/frontend.ml | 220 ++--
src/main/frontend.mli | 26 +-
src/main/main_gui.ml | 449 +++++----
src/main/main_gui.mli | 2 +-
src/main/main_text.ml | 87 +-
src/main/main_text.mli | 2 +-
src/parsing/Makefile | 9 -
src/parsing/smt_lex.mll | 150 ---
src/parsing/smt_parser.mly | 294 ------
src/parsing/smtlib2_lex.mll | 95 --
src/parsing/smtlib2_parse.mly | 315 ------
src/parsing/why_lexer.mll | 80 +-
src/parsing/why_parser.mly | 98 +-
src/preprocess/Makefile | 9 -
src/preprocess/cnf.ml | 185 ++--
src/preprocess/cnf.mli | 8 +-
src/preprocess/existantial.ml | 54 +-
src/preprocess/existantial.mli | 4 +-
src/preprocess/pruning.ml | 375 -------
src/preprocess/smt_to_why.ml | 276 -----
src/preprocess/smtlib2_to_why.ml | 533 ----------
src/preprocess/triggers.ml | 304 +++---
src/preprocess/triggers.mli | 4 +-
src/preprocess/why_typing.ml | 875 +++++++++-------
src/preprocess/why_typing.mli | 13 +-
src/sat/Makefile | 9 -
src/sat/sat_solvers.ml | 824 ++++++++++-----
src/sat/sat_solvers.mli | 21 +-
src/structures/Makefile | 9 -
src/{util/loc.ml => structures/commands.mli} | 23 +-
src/{parsing => structures}/errors.ml | 59 +-
src/{parsing => structures}/errors.mli | 16 +-
src/structures/exception.ml | 3 +-
src/structures/exception.mli | 3 +-
src/structures/explanation.ml | 48 +-
src/structures/explanation.mli | 8 +-
src/structures/formula.ml | 751 ++++++++------
src/structures/formula.mli | 81 +-
src/structures/literal.ml | 172 ++--
src/structures/literal.mli | 16 +-
src/structures/parsed.ml | 106 ++
src/structures/parsed.mli | 104 ++
src/structures/smt_ast.mli | 92 --
src/structures/smtlib2_ast.ml | 192 ----
src/structures/smtlib2_ast.mli | 131 ---
src/structures/symbols.ml | 34 +-
src/structures/symbols.mli | 16 +-
src/structures/term.ml | 178 ++--
src/structures/term.mli | 9 +-
src/structures/ty.ml | 246 +++--
src/structures/ty.mli | 21 +-
src/structures/{why_ptree.ml => typed.ml} | 189 +---
src/structures/{why_ptree.mli => typed.mli} | 146 +--
src/theories/Makefile | 9 -
src/theories/ac.ml | 133 +--
src/theories/ac.mli | 15 +-
src/theories/arith.ml | 274 +++--
src/theories/arith.mli | 10 +-
src/theories/arrays.ml | 213 ++--
src/theories/arrays.mli | 8 +-
src/theories/bitv.ml | 433 ++++----
src/theories/bitv.mli | 10 +-
src/theories/ccx.ml | 624 ++++++++++++
src/theories/{theory.mli => ccx.mli} | 43 +-
src/theories/combine.ml | 638 ++++++------
src/theories/combine.mli | 2 +-
src/theories/fm.ml | 1051 --------------------
src/theories/inequalities.ml | 366 +++++++
src/theories/inequalities.mli | 101 ++
src/theories/intervalCalculus.ml | 1033 +++++++++++++++++++
src/theories/{fm.mli => intervalCalculus.mli} | 10 +-
src/theories/intervals.ml | 223 +++--
src/theories/intervals.mli | 6 +-
src/theories/polynome.ml | 158 +--
src/theories/polynome.mli | 22 +-
src/theories/records.ml | 224 +++--
src/theories/records.mli | 6 +-
src/theories/sig.mli | 76 +-
src/theories/sum.ml | 221 ++--
src/theories/sum.mli | 6 +-
src/theories/theory.ml | 809 +++++----------
src/theories/theory.mli | 14 +-
src/theories/uf.ml | 497 +++++----
src/theories/uf.mli | 11 +-
src/theories/use.ml | 76 +-
src/theories/use.mli | 8 +-
src/util/Makefile | 9 -
src/util/hstring.ml | 12 +-
src/util/hstring.mli | 6 +-
src/util/lists.ml | 27 +
src/util/lists.mli | 18 +
src/util/loc.ml | 6 +-
src/util/loc.mli | 6 +-
src/util/myUnix.ml | 41 +
src/util/{version.mli => myUnix.mli} | 13 +-
src/util/numbers.ml | 145 +--
src/util/numbers.mli | 52 +-
src/util/{numbers.mli => numbersInterface.mli} | 92 +-
src/util/{numbers.ml => numsNumbers.ml} | 185 ++--
.../pruning.mli => util/numsNumbers.mli} | 10 +-
src/util/options.ml | 244 +++--
src/util/options.mli | 57 +-
src/util/{version.mli => profiling.ml} | 7 +-
src/util/{version.mli => profiling.mli} | 7 +-
src/util/profiling_default.ml | 131 +++
src/util/profiling_default.mli | 54 +
src/util/timers.ml | 309 ++++--
src/util/timers.mli | 85 +-
src/util/{version.mli => util.ml} | 16 +-
src/util/util.mli | 16 +
src/util/version.ml | 22 +-
src/util/version.mli | 7 +-
src/util/zarithNumbers.ml | 136 +++
src/{gui/gui_replay.mli => util/zarithNumbers.mli} | 9 +-
135 files changed, 9550 insertions(+), 9175 deletions(-)
--
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
