[Pkg-ocaml-maint-commits] [alt-ergo] branch master updated (4363a13 -> 18bc16a)
Ralf Treinen
treinen at alioth.debian.org
Tue Nov 5 15:50:32 UTC 2013
This is an automated email from the git hooks/post-receive script.
treinen pushed a change to branch master
in repository alt-ergo.
from 4363a13 debian/watch : new site @ ocamlpro
new 5dc7ee9 Imported Upstream version 0.95.2
new 51132e0 Merge tag 'upstream/0.95.2'
new 99bea10 refresh patch 0001-No-need-to-activate-debug-flag.patch
new c2476f3 drop patch 0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
new fbd9f75 drop patch 0003-Fix-a-typo.patch
new eeac213 drop patch 0004-Add-rules-and-targets-for-gui.byte.patch
new 368bca3 drop patch 0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
new 996dbd0 drop patch 0007-Fix-all-target.patch
new dca871a drop patch 0009-clean-remove-META.patch
new ba352a9 + build-dep on libzarith-ocaml-dev
new ee16ced debian/rules : drop backup of .depends
new e6907cc debian/rules : additional make targets for build and install
new f920a24 drop mandir setting in invocation of ./configure
new 15e39bf debian/rules: drop touching of configure
new 18bc16a + changelog entry: new upstream release
The 15 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:
.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 +-
debian/changelog | 23 +-
debian/control | 1 +
.../0001-No-need-to-activate-debug-flag.patch | 18 +-
...the-test-if-test.mlw-is-absent-and-use-be.patch | 24 -
debian/patches/0003-Fix-a-typo.patch | 16 -
.../0004-Add-rules-and-targets-for-gui.byte.patch | 72 -
...ma-instead-of-cmxa-for-lablgtksourceview2.patch | 42 -
debian/patches/0007-Fix-all-target.patch | 26 -
...ll-pack-into-two-separate-targets-opt-and.patch | 33 -
debian/patches/0009-clean-remove-META.patch | 17 -
debian/patches/series | 7 -
debian/rules | 19 +-
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 --------------------
177 files changed, 12595 insertions(+), 13132 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
delete mode 100644 debian/patches/0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch
delete mode 100644 debian/patches/0003-Fix-a-typo.patch
delete mode 100644 debian/patches/0004-Add-rules-and-targets-for-gui.byte.patch
delete mode 100644 debian/patches/0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
delete mode 100644 debian/patches/0007-Fix-all-target.patch
delete mode 100644 debian/patches/0008-Split-install-pack-into-two-separate-targets-opt-and.patch
delete mode 100644 debian/patches/0009-clean-remove-META.patch
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