aboutsummaryrefslogtreecommitdiff
path: root/pretyping/matching.ml
AgeCommit message (Expand)Author
2006-05-17Correcting a bug in matching context on if. jforest
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
2006-02-01Optimisation filtrage sans lieurs (utile pour Ltac)herbelin
2005-12-02Changement des named_contextgregoire
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2004-09-27collapse apps of patterns to avoid failuresbarras
2004-09-25Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...herbelin
2004-07-16Nouvelle en-têteherbelin
2003-12-16Correction bug 371 (sub_match retournait des instances non closes)herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin