aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
Commit message (Expand)AuthorAge
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Amélioration afficheur de Cases pour les constr_patternGravatar herbelin2003-06-10
* Preservation affichage des ?n en V7Gravatar herbelin2003-05-22
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)Gravatar herbelin2003-02-01
* Ajout d'un filtrage d'application partielleGravatar herbelin2003-01-31
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* 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
* 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