aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
Commit message (Expand)AuthorAge
* Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)Gravatar herbelin2001-09-14
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* entetesGravatar filliatr2001-03-15
* 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