This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository alt-ergo.
commit 51132e01b1ea88245020fd77691f006cd8bc3f3b
Merge: 4363a13 5dc7ee9
Author: Ralf Treinen <trei...@pps.univ-paris-diderot.fr>
Date: Tue Nov 5 14:07:06 2013 +0100
Merge tag 'upstream/0.95.2'
Upstream version 0.95.2
.depend | 263 ----
CHANGES | 11 +
COPYING | 17 +-
INSTALL | 35 +-
CeCILL-C => LICENSE | 0
Makefile.in | 473 ++++---
README | 36 -
existantial.mli => README.md | 48 +-
arith.ml | 592 ---------
cc.ml | 719 ----------
cnf.ml | 422 ------
common.ml | 257 ----
configure | 82 +-
configure.in | 66 +-
doc/ergoheader.txt | 16 +
{util => doc}/gtk-lang/alt-ergo.lang | 0
doc/headache_config.txt | 14 +
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 --------------
gui_replay.mli | 4 -
instantiation.ml | 470 -------
instantiation.mli | 54 -
matching.ml | 341 -----
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 --
revision.sh | 31 -
smtlib2_util.ml | 31 -
src/Makefile | 9 +
src/gui/Makefile | 9 +
gui_replay.ml => src/gui/gui_replay.ml | 22 +-
combine.mli => src/gui/gui_replay.mli | 38 +-
gui_session.ml => src/gui/gui_session.ml | 33 +-
gui_session.mli => src/gui/gui_session.mli | 33 +-
why_annoted.ml => src/gui/why_annoted.ml | 896 +++++++------
why_annoted.mli => src/gui/why_annoted.mli | 45 +-
why_connected.ml => src/gui/why_connected.ml | 720 +++++-----
why_connected.mli => src/gui/why_connected.mli | 33 +-
src/instances/Makefile | 9 +
src/instances/matching.ml | 381 ++++++
matching.mli => src/instances/matching.mli | 36 +-
src/main/Makefile | 9 +
frontend.ml => src/main/frontend.ml | 177 ++-
frontend.mli => src/main/frontend.mli | 42 +-
gui.ml => src/main/main_gui.ml | 939 ++++++-------
combine.mli => src/main/main_gui.mli | 35 +-
main.ml => src/main/main_text.ml | 58 +-
combine.mli => src/main/main_text.mli | 35 +-
src/parsing/Makefile | 9 +
src/parsing/errors.ml | 137 ++
common.mli => src/parsing/errors.mli | 59 +-
smt_lex.mll => src/parsing/smt_lex.mll | 33 +-
smt_parser.mly => src/parsing/smt_parser.mly | 33 +-
smtlib2_lex.mll => src/parsing/smtlib2_lex.mll | 38 +-
smtlib2_parse.mly => src/parsing/smtlib2_parse.mly | 33 +-
why_lexer.mll => src/parsing/why_lexer.mll | 77 +-
why_parser.mly => src/parsing/why_parser.mly | 176 ++-
src/preprocess/Makefile | 9 +
src/preprocess/cnf.ml | 420 ++++++
cnf.mli => src/preprocess/cnf.mli | 35 +-
existantial.ml => src/preprocess/existantial.ml | 61 +-
existantial.mli => src/preprocess/existantial.mli | 33 +-
pruning.ml => src/preprocess/pruning.ml | 351 +++--
pruning.mli => src/preprocess/pruning.mli | 33 +-
smt_to_why.ml => src/preprocess/smt_to_why.ml | 221 ++--
.../preprocess/smtlib2_to_why.ml | 106 +-
triggers.ml => src/preprocess/triggers.ml | 710 +++++-----
triggers.mli => src/preprocess/triggers.mli | 34 +-
src/preprocess/why_typing.ml | 1374 +++++++++++++++++++
why_typing.mli => src/preprocess/why_typing.mli | 33 +-
src/sat/Makefile | 9 +
sat.ml => src/sat/sat.ml | 572 ++++----
sat.mli => src/sat/sat.mli | 33 +-
src/structures/Makefile | 9 +
exception.ml => src/structures/exception.ml | 33 +-
exception.mli => src/structures/exception.mli | 33 +-
src/structures/explanation.ml | 118 ++
explanation.mli => src/structures/explanation.mli | 35 +-
formula.ml => src/structures/formula.ml | 325 ++---
formula.mli => src/structures/formula.mli | 33 +-
literal.ml => src/structures/literal.ml | 165 ++-
literal.mli => src/structures/literal.mli | 35 +-
smt_ast.mli => src/structures/smt_ast.mli | 45 +-
smtlib2_ast.ml => src/structures/smtlib2_ast.ml | 39 +-
src/structures/smtlib2_ast.mli | 125 ++
subst.ml => src/structures/subst.ml | 33 +-
subst.mli => src/structures/subst.mli | 33 +-
symbols.ml => src/structures/symbols.ml | 48 +-
symbols.mli => src/structures/symbols.mli | 37 +-
term.ml => src/structures/term.ml | 144 +-
term.mli => src/structures/term.mli | 37 +-
ty.ml => src/structures/ty.ml | 291 ++--
ty.mli => src/structures/ty.mli | 55 +-
why_ptree.mli => src/structures/why_ptree.ml | 141 +-
why_ptree.mli => src/structures/why_ptree.mli | 50 +-
src/theories/Makefile | 9 +
ac.ml => src/theories/ac.ml | 165 +--
ac.mli => src/theories/ac.mli | 34 +-
src/theories/arith.ml | 552 ++++++++
arith.mli => src/theories/arith.mli | 33 +-
arrays.ml => src/theories/arrays.ml | 225 ++--
arrays.mli => src/theories/arrays.mli | 33 +-
bitv.ml => src/theories/bitv.ml | 525 ++++----
bitv.mli => src/theories/bitv.mli | 33 +-
boxed.ml => src/theories/boxed.ml | 35 +-
boxed.mli => src/theories/boxed.mli | 35 +-
src/theories/cc.ml | 726 ++++++++++
cc.mli => src/theories/cc.mli | 35 +-
combine.ml => src/theories/combine.ml | 139 +-
combine.mli => src/theories/combine.mli | 33 +-
custom_theory.ml => src/theories/custom_theory.ml | 77 +-
.../theories/custom_theory.mli | 35 +-
src/theories/fm.ml | 1034 +++++++++++++++
fm.mli => src/theories/fm.mli | 33 +-
incr_match.ml => src/theories/incr_match.ml | 133 +-
incr_match.mli => src/theories/incr_match.mli | 34 +-
src/theories/instantiation.ml | 468 +++++++
src/theories/instantiation.mli | 53 +
intervals.ml => src/theories/intervals.ml | 423 +++---
intervals.mli => src/theories/intervals.mli | 50 +-
polynome.ml => src/theories/polynome.ml | 256 ++--
polynome.mli => src/theories/polynome.mli | 62 +-
records.ml => src/theories/records.ml | 249 ++--
records.mli => src/theories/records.mli | 33 +-
sig.mli => src/theories/sig.mli | 111 +-
sum.ml => src/theories/sum.ml | 293 +++--
sum.mli => src/theories/sum.mli | 33 +-
uf.ml => src/theories/uf.ml | 434 +++---
uf.mli => src/theories/uf.mli | 34 +-
use.ml => src/theories/use.ml | 64 +-
use.mli => src/theories/use.mli | 39 +-
src/util/Makefile | 9 +
hashcons.ml => src/util/hashcons.ml | 82 +-
hashcons.mli => src/util/hashcons.mli | 149 +--
hstring.ml => src/util/hstring.ml | 47 +-
hstring.mli => src/util/hstring.mli | 38 +-
loc.ml => src/util/loc.ml | 39 +-
combine.mli => src/util/loc.mli | 37 +-
src/util/numbers.ml | 159 +++
src/util/numbers.mli | 63 +
src/util/options.ml | 334 +++++
options.mli => src/util/options.mli | 217 ++-
timers.ml => src/util/timers.ml | 37 +-
timers.mli => src/util/timers.mli | 33 +-
combine.mli => src/util/version.mli | 37 +-
why_typing.ml | 1390 --------------------
165 files changed, 12563 insertions(+), 12866 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
