aboutsummaryrefslogtreecommitdiff
path: root/pretyping/matching.mli
AgeCommit message (Expand)Author
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
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