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