aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.mli
Commit message (Expand)AuthorAge
* appel de Simplify depuis CoqGravatar coq2005-03-18
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ground Update.Gravatar corbinea2003-06-20
* Ground and CCsolve updatesGravatar corbinea2003-05-25
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Added the Ground tactic.Gravatar corbinea2003-04-25
* Correction of a bug in Intuition (no more decomposition of dependent pairs).Gravatar corbinea2002-05-22
* eclaircissement du codeGravatar courant2001-09-13
* entetesGravatar filliatr2001-03-15
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout get_referenceGravatar herbelin2000-05-03
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28