index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
recordops.mli
Commit message (
Expand
)
Author
Age
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
GROS COMMIT:
barras
2001-11-05
*
Nettoyage Recordobj et conséquences
herbelin
2001-10-16
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
entetes
filliatr
2001-03-15
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Export fonction testant si un inductive est un record
herbelin
2000-12-19
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Ajout de Record
herbelin
2000-01-11
*
- global_reference traite des variables
filliatr
1999-12-03
*
Versions initiales
herbelin
1999-11-24