aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
Commit message (Expand)AuthorAge
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* bug serieux efficacite de ltacGravatar barras2006-06-19
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* HUGE COMMITGravatar sacerdot2005-01-03
* The type Pattern.constr_label was isomorphic to Libnames.global_reference.Gravatar sacerdot2004-12-07
* MAJ PCoFixGravatar herbelin2004-11-26
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Substitution dans REvar et PEvar plutot que encodage via noeud application po...Gravatar herbelin2003-12-19
* 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