aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/matching.mli
Commit message (Expand)AuthorAge
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 06:13:23 +0000