]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/equalityTactics.ml
coercion application
[helm.git] / helm / ocaml / tactics / equalityTactics.ml
2004-12-01 Enrico TassiAdded universes handling. The PRE_UNIVERSES tag may...
2004-11-29 Stefano Zacchirolipasses ~subst to FreshNameGenerator
2004-06-01 Enrico Tassinew universes implementation
2004-04-20 Stefano Zacchiroligot rid of ~status label so that tactics can now be...
2004-02-24 Claudio Sacerdoti... Partial porting to V8 URIs.
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.
2004-01-27 Stefano Zacchirolis/List.find.../CicUtil.lookup_meta/
2004-01-22 Stefano Zacchirolimoved hard coded uris to HelmLibraryObjects
2003-12-02 Ferruccio Guidisort CProp added
2003-09-05 Claudio Sacerdoti... Replace is now working also over Type.
2003-09-05 Claudio Sacerdoti... Replace tactic fixed. It was not working any longer...
2003-06-19 Claudio Sacerdoti... Merge of the V7_3_new_exportation branch.