aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/matching.ml
Commit message (Expand)AuthorAge
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* 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