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
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
Open notation for declaring record instances.
msozeau
2008-10-23
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...
msozeau
2008-01-17
*
Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...
msozeau
2007-12-31
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Pas d'escamotage des noms réservés si Set Printing All actibvé
herbelin
2006-12-08
*
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