]> matita.cs.unibo.it Git - helm.git/history - components/tactics/proofEngineHelpers.ml
- ProofEngineHelpers: namer_of moved to GrafiteEngine
[helm.git] / components / tactics / proofEngineHelpers.ml
2007-11-13 Ferruccio Guidi- ProofEngineHelpers: namer_of moved to GrafiteEngine
2007-11-02 Ferruccio Guidi- tacticals: new tactical ifs added: uses thens where...
2007-10-28 Claudio Sacerdoti... Pretty-printing of "match ... with" pattern syntax...
2007-08-22 Claudio Sacerdoti... select now works correctly even if multiple hypotheses...
2007-07-20 Ferruccio Guidiacic_procedural: bug fix:
2007-05-17 Enrico Tassiadded a (for the moment) dummy field _subst to Proofeng...
2007-05-17 Enrico Tassiauto rewritten with only one tail recursive function.
2007-03-16 Ferruccio Guidielim tactic: it needs two arguments, a term as well...
2007-01-10 Ferruccio Guidiattributes now in the proof status: commit 2
2006-12-14 Claudio Sacerdoti... Huge commit:
2006-11-15 Ferruccio Guiditranscript updated
2006-08-28 Ferruccio Guidi- Level-1: some fixes to the extraction procedure
2006-06-28 Ferruccio Guidi- "linear" flag added to lapply (automatic clearing)
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/