index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
matching.mli
Commit message (
Expand
)
Author
Age
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
Quelques modifications autour du filtrage Ltac:
herbelin
2008-07-16
*
Add possibility to match on defined hypotheses, using brackets to
msozeau
2008-06-16
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...
herbelin
2004-09-25
*
Nouvelle en-tête
herbelin
2004-07-16
*
Correction bug 371 (sub_match retournait des instances non closes)
herbelin
2003-12-16
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07