aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
AgeCommit message (Expand)Author
2001-11-05GROS COMMIT:barras
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
2001-05-29Facilites pour le debogguage des univers.coq
2001-03-15entetesfilliatr
2001-03-01nouvelle implantation de la reductionbarras
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin