aboutsummaryrefslogtreecommitdiff
path: root/pretyping/matching.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2005-01-21Compatibilité ocamlweb pour cible docherbelin
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