]> matita.cs.unibo.it Git - helm.git/commit
Big bug fixed: batchParser applied the varsprefix prefix also to
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Mar 2004 18:56:53 +0000 (18:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Mar 2004 18:56:53 +0000 (18:56 +0000)
commit6cfcba76baa8f30c42624e911bd34a702f785766
tree6c222ac2f8bac9226850161e6a81befb92682aee
parent5e1c4e50b88cd1b75a14a34b93297a3aba6af890
Big bug fixed: batchParser applied the varsprefix prefix also to
constants and inductive types!!!

It is now possible to specify independently the prefix for variables and
the prefix for all the other objects.
helm/gTopLevel/batchParser.ml
helm/gTopLevel/batchParser.mli
helm/gTopLevel/regtest.ml
helm/gTopLevel/testlibrary.ml