matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/freshNamesGenerator.ml

2005-05-27	Enrico Tassi	removed debug prerr_endline	blob \| commitdiff \| raw
2004-12-01	Enrico Tassi	Added universes handling. The PRE_UNIVERSES tag may...	blob \| commitdiff \| raw \| diff to current
2004-11-29	Stefano Zacchiroli	bugfix: FreshNameGenerator uses the type checker on...	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	"assert false" relaxed to a warning.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	- the result of a refinement is now cleared from dummy...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	dummy dependent types and dummy letins are now removed...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	fresh_name_generator has now also the metasenv parameter.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	mk_fresh_name moved to FreshNamesGenerator.	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.