aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/matching.ml
Commit message (Expand)AuthorAge
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Applatissement des noeuds application vide dans le filtrage Ltac (ex:Gravatar herbelin2006-10-25
* Correcting a bug in matching context on if. Gravatar jforest2006-05-17
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
* 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