aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
AgeCommit message (Expand)Author
2003-02-01Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)herbelin
2003-01-31Ajout d'un filtrage d'application partielleherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-01Vraie substitutivite de autohintscoq
2002-08-02Modules dans COQ\!\!\!\!coq
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:20:28 +0000