aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
Commit message (Expand)AuthorAge
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Code mortGravatar herbelin2000-06-15
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajout get_referenceGravatar herbelin2000-05-03
* DiversGravatar herbelin2000-05-02
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28