index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
reserve.ml
Age
Commit message (
Expand
)
Author
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-08-13
Death of "survive_module" and "survive_section" (the first one was
herbelin
2008-11-05
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-10-23
Open notation for declaring record instances.
msozeau
2008-03-28
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-01-17
Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...
msozeau
2007-12-31
Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...
msozeau
2007-12-06
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-05
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-03-19
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2006-12-08
Pas d'escamotage des noms réservés si Set Printing All actibvé
herbelin
2006-04-27
Standardisation nom option_app en option_map
herbelin
2005-12-26
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-02
Changement des named_context
gregoire
2004-09-15
hiding the meta_map in evar_defs
barras
2004-07-16
Nouvelle en-tête
herbelin
2004-03-05
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-01-02
meilleure presentation des commentaires du traducteur
barras
2003-12-19
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-10-07
Correction du bug 335 et Export/Require Export dans un module
coq
2003-09-10
Renommage des variables '_'
herbelin
2003-09-09
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-08-11
Ajout LetTuple
herbelin
2003-08-11
Nouvelle mouture du traducteur v7->v8
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-03-29
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin