]> 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)
commita1c4c601850c71e094a4703af00f02ca2026d8ed
tree64e9a4cda71a565d255a11c20d95ac5e4014c2f1
parentc30b48dc423ef9c25473d7b5f211eac018f2f0fa
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:
components/acic_procedural/.depend
components/acic_procedural/.depend.opt
components/tactics/auto.ml
components/tactics/auto.mli
components/tactics/autoCache.ml
components/tactics/autoTypes.ml
components/tactics/autoTypes.mli
components/tactics/proofEngineHelpers.ml
components/tactics/proofEngineHelpers.mli
matita/.depend
matita/library/decidable_kit/decidable.ma
matita/library/demo/power_derivative.ma
matita/library/nat/factorization.ma
matita/library_auto/auto/Z/times.ma
matita/library_auto/auto/nat/congruence.ma
matita/library_auto/auto/nat/euler_theorem.ma
matita/library_auto/auto/nat/factorization.ma
matita/library_auto/auto/nat/fermat_little_theorem.ma
matita/library_auto/auto/nat/gcd.ma
matita/library_auto/auto/nat/nth_prime.ma
matita/library_auto/auto/nat/ord.ma
matita/library_auto/auto/nat/primes.ma
matita/matita.glade
matita/matita.ml
matita/matitaAutoGui.ml [new file with mode: 0644]