]> matita.cs.unibo.it Git - helm.git/commit
1) removed many debug prints
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Wed, 21 Sep 2011 14:56:17 +0000 (14:56 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Wed, 21 Sep 2011 14:56:17 +0000 (14:56 +0000)
commit4f3b04e9966484011328d5b0eb358da4416e29b0
tree7e9103ba4298eddfe602105a775c1623148e2d96
parentd0d2ebcf0ad48c38dcd69142f5e080e987fc5536
1) removed many debug prints
2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).
17 files changed:
matitaB/components/content_pres/termContentPres.ml
matitaB/components/ng_library/nCicLibrary.ml
matitaB/components/ng_paramodulation/nCicBlob.ml
matitaB/components/ng_paramodulation/nCicParamod.ml
matitaB/components/ng_paramodulation/nCicParamod.mli
matitaB/components/ng_paramodulation/paramod.ml
matitaB/components/ng_paramodulation/paramod.mli
matitaB/components/ng_paramodulation/stats.ml
matitaB/components/ng_paramodulation/superposition.ml
matitaB/components/ng_paramodulation/terms.ml
matitaB/components/ng_paramodulation/terms.mli
matitaB/components/ng_tactics/nTacStatus.ml
matitaB/matita/index.html
matitaB/matita/matitadaemon.ml
matitaB/matita/matitaweb.css
matitaB/matita/matitaweb.js
matitaB/matita/netplex.conf