]> matita.cs.unibo.it Git - helm.git/commit
Typing of intros_tac improved. It now has a parameter that is a fresh-names
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 17:47:30 +0000 (17:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Dec 2002 17:47:30 +0000 (17:47 +0000)
commit9597e7e79ce0606671f8aa170951d119419780ad
tree590b4fdd6ca7f1b94c519e8980df0f7b1cf7ff35
parent0cc3da0c46191687bad5104b9947d311f1ad6918
Typing of intros_tac improved. It now has a parameter that is a fresh-names
generator.
helm/gTopLevel/fourierR.ml
helm/gTopLevel/primitiveTactics.ml
helm/gTopLevel/primitiveTactics.mli
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/variousTactics.ml