aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/matching.ml
Commit message (Expand)AuthorAge
* Optimisation filtrage sans lieurs (utile pour Ltac)Gravatar herbelin2006-02-01
* Changement des named_contextGravatar gregoire2005-12-02
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* collapse apps of patterns to avoid failuresGravatar barras2004-09-27
* Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...Gravatar herbelin2004-09-25
* Nouvelle en-têteGravatar herbelin2004-07-16
* Correction bug 371 (sub_match retournait des instances non closes)Gravatar herbelin2003-12-16
* 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