aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/matching.mli
Commit message (Expand)AuthorAge
* Pushing lazy lists into Ltac. Now, the control flow is explicitGravatar ppedrot2013-05-28
* Code cleaning in Matching.Gravatar ppedrot2013-05-24
* Fixing ocamldoc compilation.Gravatar ppedrot2013-05-06
* Matching patterns: fixed allow_partial_app which was not working onGravatar herbelin2013-04-17
* Modulification of identifierGravatar ppedrot2012-12-14
* Adapt pieces of code needing -rectypesGravatar letouzey2012-10-06
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* 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