]> matita.cs.unibo.it Git - helm.git/commit
auto rewritten with only one tail recursive function.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)
commit750d027aedc76aac9def8885dc2bdb6ccdc049d9
treed847f72b5a0d6b0788db244246e4ca625d9bf053
parent2c40b39e14811c380e03bdd876ec1591f30da911
auto rewritten with only one tail recursive function.
this allows to have a GUI to drive the procedure.
a new measure size has been added, and width changed its meaning.
a bunch of unfold lt added to library_auto.
25 files changed:
helm/software/components/acic_procedural/.depend
helm/software/components/acic_procedural/.depend.opt
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoCache.ml
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/autoTypes.mli
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/matita/.depend
helm/software/matita/library/decidable_kit/decidable.ma
helm/software/matita/library/demo/power_derivative.ma
helm/software/matita/library/nat/factorization.ma
helm/software/matita/library_auto/auto/Z/times.ma
helm/software/matita/library_auto/auto/nat/congruence.ma
helm/software/matita/library_auto/auto/nat/euler_theorem.ma
helm/software/matita/library_auto/auto/nat/factorization.ma
helm/software/matita/library_auto/auto/nat/fermat_little_theorem.ma
helm/software/matita/library_auto/auto/nat/gcd.ma
helm/software/matita/library_auto/auto/nat/nth_prime.ma
helm/software/matita/library_auto/auto/nat/ord.ma
helm/software/matita/library_auto/auto/nat/primes.ma
helm/software/matita/matita.glade
helm/software/matita/matita.ml
helm/software/matita/matitaAutoGui.ml [new file with mode: 0644]