[Pkg-ocaml-maint-commits] [alt-ergo] branch experimental/upstream updated (e8667c8 -> da20a0b)
Ralf Treinen
treinen at moszumanska.debian.org
Tue Dec 30 18:13:28 UTC 2014
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
More information about the Pkg-ocaml-maint-commits
mailing list