[Pkg-ocaml-maint-commits] [alt-ergo] branch upstream updated (e8667c8 -> 5dc7ee9)
Ralf Treinen
treinen at alioth.debian.org
Thu Nov 7 15:49:23 UTC 2013
This is an automated email from the git hooks/post-receive script.
treinen pushed a change to branch upstream
in repository alt-ergo.
from e8667c8 Imported Upstream version 0.95.1
adds 5dc7ee9 Imported Upstream version 0.95.2
No new revisions were added by this update.
Summary of changes:
.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(-)
delete mode 100644 .depend
rename CeCILL-C => LICENSE (100%)
delete mode 100644 README
copy existantial.mli => README.md (59%)
delete mode 100644 arith.ml
delete mode 100644 cc.ml
delete mode 100644 cnf.ml
delete mode 100644 common.ml
create mode 100644 doc/ergoheader.txt
rename {util => doc}/gtk-lang/alt-ergo.lang (100%)
create mode 100644 doc/headache_config.txt
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 gui_replay.mli
delete mode 100644 instantiation.ml
delete mode 100644 instantiation.mli
delete mode 100644 matching.ml
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 100755 revision.sh
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 (63%)
copy combine.mli => src/gui/gui_replay.mli (63%)
rename gui_session.ml => src/gui/gui_session.ml (88%)
rename gui_session.mli => src/gui/gui_session.mli (73%)
rename why_annoted.ml => src/gui/why_annoted.ml (68%)
rename why_annoted.mli => src/gui/why_annoted.mli (93%)
rename why_connected.ml => src/gui/why_connected.ml (64%)
rename why_connected.mli => src/gui/why_connected.mli (75%)
create mode 100644 src/instances/Makefile
create mode 100644 src/instances/matching.ml
rename matching.mli => src/instances/matching.mli (77%)
create mode 100644 src/main/Makefile
rename frontend.ml => src/main/frontend.ml (61%)
rename frontend.mli => src/main/frontend.mli (73%)
rename gui.ml => src/main/main_gui.ml (62%)
copy combine.mli => src/main/main_gui.mli (63%)
rename main.ml => src/main/main_text.ml (52%)
copy combine.mli => src/main/main_text.mli (63%)
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 (89%)
rename smt_parser.mly => src/parsing/smt_parser.mly (93%)
rename smtlib2_lex.mll => src/parsing/smtlib2_lex.mll (83%)
rename smtlib2_parse.mly => src/parsing/smtlib2_parse.mly (94%)
rename why_lexer.mll => src/parsing/why_lexer.mll (76%)
rename why_parser.mly => src/parsing/why_parser.mly (67%)
create mode 100644 src/preprocess/Makefile
create mode 100644 src/preprocess/cnf.ml
rename cnf.mli => src/preprocess/cnf.mli (72%)
rename existantial.ml => src/preprocess/existantial.ml (76%)
rename existantial.mli => src/preprocess/existantial.mli (66%)
rename pruning.ml => src/preprocess/pruning.ml (50%)
rename pruning.mli => src/preprocess/pruning.mli (67%)
rename smt_to_why.ml => src/preprocess/smt_to_why.ml (53%)
rename smtlib2_to_why.ml => src/preprocess/smtlib2_to_why.ml (90%)
rename triggers.ml => src/preprocess/triggers.ml (51%)
rename triggers.mli => src/preprocess/triggers.mli (70%)
create mode 100644 src/preprocess/why_typing.ml
rename why_typing.mli => src/preprocess/why_typing.mli (71%)
create mode 100644 src/sat/Makefile
rename sat.ml => src/sat/sat.ml (50%)
rename sat.mli => src/sat/sat.mli (78%)
create mode 100644 src/structures/Makefile
rename exception.ml => src/structures/exception.ml (68%)
rename exception.mli => src/structures/exception.mli (68%)
create mode 100644 src/structures/explanation.ml
rename explanation.mli => src/structures/explanation.mli (76%)
rename formula.ml => src/structures/formula.ml (66%)
rename formula.mli => src/structures/formula.mli (83%)
rename literal.ml => src/structures/literal.ml (59%)
rename literal.mli => src/structures/literal.mli (79%)
rename smt_ast.mli => src/structures/smt_ast.mli (82%)
rename smtlib2_ast.ml => src/structures/smtlib2_ast.ml (90%)
create mode 100644 src/structures/smtlib2_ast.mli
rename subst.ml => src/structures/subst.ml (73%)
rename subst.mli => src/structures/subst.mli (71%)
rename symbols.ml => src/structures/symbols.ml (85%)
rename symbols.mli => src/structures/symbols.mli (78%)
rename term.ml => src/structures/term.ml (69%)
rename term.mli => src/structures/term.mli (76%)
rename ty.ml => src/structures/ty.ml (64%)
rename ty.mli => src/structures/ty.mli (74%)
copy why_ptree.mli => src/structures/why_ptree.ml (63%)
rename why_ptree.mli => src/structures/why_ptree.mli (89%)
create mode 100644 src/theories/Makefile
rename ac.ml => src/theories/ac.ml (69%)
rename ac.mli => src/theories/ac.mli (81%)
create mode 100644 src/theories/arith.ml
rename arith.mli => src/theories/arith.mli (69%)
rename arrays.ml => src/theories/arrays.ml (73%)
rename arrays.mli => src/theories/arrays.mli (69%)
rename bitv.ml => src/theories/bitv.ml (65%)
rename bitv.mli => src/theories/bitv.mli (69%)
rename boxed.ml => src/theories/boxed.ml (82%)
rename boxed.mli => src/theories/boxed.mli (76%)
create mode 100644 src/theories/cc.ml
rename cc.mli => src/theories/cc.mli (70%)
rename combine.ml => src/theories/combine.ml (85%)
copy combine.mli => src/theories/combine.mli (65%)
rename custom_theory.ml => src/theories/custom_theory.ml (93%)
rename custom_theory.mli => src/theories/custom_theory.mli (74%)
create mode 100644 src/theories/fm.ml
rename fm.mli => src/theories/fm.mli (69%)
rename incr_match.ml => src/theories/incr_match.ml (84%)
rename incr_match.mli => src/theories/incr_match.mli (74%)
create mode 100644 src/theories/instantiation.ml
create mode 100644 src/theories/instantiation.mli
rename intervals.ml => src/theories/intervals.ml (66%)
rename intervals.mli => src/theories/intervals.mli (61%)
rename polynome.ml => src/theories/polynome.ml (50%)
rename polynome.mli => src/theories/polynome.mli (68%)
rename records.ml => src/theories/records.ml (70%)
rename records.mli => src/theories/records.mli (69%)
rename sig.mli => src/theories/sig.mli (73%)
rename sum.ml => src/theories/sum.ml (57%)
rename sum.mli => src/theories/sum.mli (69%)
rename uf.ml => src/theories/uf.ml (72%)
rename uf.mli => src/theories/uf.mli (78%)
rename use.ml => src/theories/use.ml (74%)
rename use.mli => src/theories/use.mli (75%)
create mode 100644 src/util/Makefile
rename hashcons.ml => src/util/hashcons.ml (77%)
rename hashcons.mli => src/util/hashcons.mli (52%)
rename hstring.ml => src/util/hstring.ml (67%)
rename hstring.mli => src/util/hstring.mli (69%)
rename loc.ml => src/util/loc.ml (64%)
copy combine.mli => src/util/loc.mli (63%)
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 (65%)
rename timers.ml => src/util/timers.ml (83%)
rename timers.mli => src/util/timers.mli (71%)
rename combine.mli => src/util/version.mli (63%)
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
More information about the Pkg-ocaml-maint-commits
mailing list