index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
reserve.ml
Commit message (
Expand
)
Author
Age
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
Nouvelle en-tête
herbelin
2004-07-16
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Renommage des variables '_'
herbelin
2003-09-10
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Ajout LetTuple
herbelin
2003-08-11
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29