]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/primitiveTactics.ml
Universes introduction
[helm.git] / helm / ocaml / tactics / primitiveTactics.ml
2004-04-23 Enrico TassiUniverses introduction
2004-04-22 Claudio Sacerdoti... Patches to generate ?1 : ?2 : Type in place of ?1 ...
2004-04-20 Stefano Zacchiroligot rid of ~status label so that tactics can now be...
2004-04-06 Stefano Zacchirolibugfix: local context and canonical context previously...
2004-04-06 Stefano Zacchirolibugfix: the function that abstract constant occurrences...
2004-03-24 Stefano ZacchiroliCSC: hack to make applications of constants that have...
2004-02-12 Stefano Zacchiroliremoved some anciente debugging messages
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit
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-02-02 Stefano Zacchirolichanged prototype of CicMetaSubst.apply_subst*
2004-01-27 Stefano Zacchirolis/List.find.../CicUtil.lookup_meta/
2004-01-22 Stefano Zacchiroliported to cicMetaSubst
2003-12-02 Ferruccio Guidisort CProp added
2003-09-05 Claudio Sacerdoti... Defs in context may now have an optional type (when...
2003-06-19 Claudio Sacerdoti... Merge of the V7_3_new_exportation branch.