aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
Commit message (Expand)AuthorAge
* nouvelle implantation de la reductionGravatar barras2001-03-01
* uniformisation avec constr des lieurs dans rawterm/patternGravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26