]> matita.cs.unibo.it Git - helm.git/commit
fresh_name_generator has now also the metasenv parameter.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 11:54:14 +0000 (11:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 11:54:14 +0000 (11:54 +0000)
commitfeb3c287997f7d35747c12e0db62e6194f5587a3
treefd2cf84c8a13196131c54bb3f0a4e9b6e6ab4204
parent7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5
fresh_name_generator has now also the metasenv parameter.
Before this patch it used the empty metasenv (and it worked, somehow!)
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/invokeTactics.ml
helm/gTopLevel/invokeTactics.mli
helm/ocaml/cic_unification/.depend
helm/ocaml/cic_unification/freshNamesGenerator.ml
helm/ocaml/cic_unification/freshNamesGenerator.mli
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineTypes.ml
helm/ocaml/tactics/variousTactics.ml