]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/freshNamesGenerator.ml
ported to Dbi-disambiguation
[helm.git] / helm / ocaml / cic_unification / freshNamesGenerator.ml
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit
2004-02-05 Claudio Sacerdoti... "assert false" relaxed to a warning.
2004-02-05 Claudio Sacerdoti... - the result of a refinement is now cleared from dummy...
2004-02-05 Claudio Sacerdoti... dummy dependent types and dummy letins are now removed...
2004-02-05 Claudio Sacerdoti... fresh_name_generator has now also the metasenv parameter.
2004-02-05 Claudio Sacerdoti... mk_fresh_name moved to FreshNamesGenerator.