aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.mli
Commit message (Expand)AuthorAge
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)Gravatar herbelin2001-09-14
* entetesGravatar filliatr2001-03-15
* 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
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26