index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pattern.mli
Commit message (
Expand
)
Author
Age
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixed a bug introduced in a combination in r12807 and revealed in
herbelin
2010-06-28
*
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
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Opened the possibility to type Ltac patterns but it is not fully functional yet
herbelin
2009-12-24
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
bug serieux efficacite de ltac
barras
2006-06-19
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Timide tentative de clarification du statut de l'opérateur de filtrage
herbelin
2006-04-24
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
sacerdot
2004-12-07
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
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
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Vraie substitutivite de autohints
coq
2002-10-01
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)
herbelin
2001-09-14
*
entetes
filliatr
2001-03-15
*
uniformisation avec constr des lieurs dans rawterm/pattern
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Pattern sera mieux dans Pretyping; relâchement head_pattern_bound
herbelin
2000-12-26