This is an automated email from the git hooks/post-receive script.
treinen pushed a change to branch master
in repository alt-ergo.
from e19d02d upload to sid
new c7774aa d/watch: version 4; pgpsigurlmangle
new f60d17b Imported Upstream version 1.01
new 5fc61c2 Merge tag 'upstream/1.01'
new 34925bc new upstream
new 0baf076 refreshed patches
new 1e9a2bb standards-version 3.9.7
The 6 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:
CHANGES | 187 ++++
INSTALL.md | 40 +-
Makefile.configurable.in | 3 +-
Makefile.users | 119 ++-
README.md | 2 +-
configure | 89 +-
configure.in | 42 +-
debian/changelog | 8 +
debian/control | 2 +-
debian/patches/0001-dont-activate-debug-flag | 6 +-
debian/patches/0002-non-free-dropped | 75 +-
debian/patches/0003-allow-set-build-date | 24 +-
debian/watch | 9 +-
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 +-
141 files changed, 9644 insertions(+), 9205 deletions(-)
delete mode 100644 src/Makefile
delete mode 100644 src/gui/Makefile
delete mode 100644 src/instances/Makefile
delete mode 100644 src/main/Makefile
delete mode 100644 src/parsing/Makefile
delete mode 100644 src/parsing/smt_lex.mll
delete mode 100644 src/parsing/smt_parser.mly
delete mode 100644 src/parsing/smtlib2_lex.mll
delete mode 100644 src/parsing/smtlib2_parse.mly
delete mode 100644 src/preprocess/Makefile
delete mode 100644 src/preprocess/pruning.ml
delete mode 100644 src/preprocess/smt_to_why.ml
delete mode 100644 src/preprocess/smtlib2_to_why.ml
delete mode 100644 src/sat/Makefile
delete mode 100644 src/structures/Makefile
copy src/{util/loc.ml => structures/commands.mli} (80%)
rename src/{parsing => structures}/errors.ml (86%)
rename src/{parsing => structures}/errors.mli (90%)
create mode 100644 src/structures/parsed.ml
create mode 100644 src/structures/parsed.mli
delete mode 100644 src/structures/smt_ast.mli
delete mode 100644 src/structures/smtlib2_ast.ml
delete mode 100644 src/structures/smtlib2_ast.mli
rename src/structures/{why_ptree.ml => typed.ml} (61%)
rename src/structures/{why_ptree.mli => typed.mli} (53%)
delete mode 100644 src/theories/Makefile
create mode 100644 src/theories/ccx.ml
copy src/theories/{theory.mli => ccx.mli} (68%)
delete mode 100644 src/theories/fm.ml
create mode 100644 src/theories/inequalities.ml
create mode 100644 src/theories/inequalities.mli
create mode 100644 src/theories/intervalCalculus.ml
rename src/theories/{fm.mli => intervalCalculus.mli} (91%)
delete mode 100644 src/util/Makefile
create mode 100644 src/util/lists.ml
create mode 100644 src/util/lists.mli
create mode 100644 src/util/myUnix.ml
copy src/util/{version.mli => myUnix.mli} (54%)
copy src/util/{numbers.mli => numbersInterface.mli} (55%)
copy src/util/{numbers.ml => numsNumbers.ml} (50%)
rename src/{preprocess/pruning.mli => util/numsNumbers.mli} (84%)
copy src/util/{version.mli => profiling.ml} (69%)
copy src/util/{version.mli => profiling.mli} (69%)
create mode 100644 src/util/profiling_default.ml
create mode 100644 src/util/profiling_default.mli
copy src/util/{version.mli => util.ml} (50%)
create mode 100644 src/util/util.mli
create mode 100644 src/util/zarithNumbers.ml
copy src/{gui/gui_replay.mli => util/zarithNumbers.mli} (84%)
--
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
