index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
recordops.mli
Age
Commit message (
Expand
)
Author
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-26
Misc small fixes : warning, dep cycles, ocamlbuild...
letouzey
2009-11-04
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-01-17
DISCLAIMER
puech
2008-11-05
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-08-05
Suite 11187 et 11298 : ne retarder le dépliage d'une projection
herbelin
2008-06-29
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-02-19
added products and sorts as possible heads for canonical structures
corbinea
2008-02-14
Added default canonical structures (see example in test-suite)
corbinea
2006-08-24
Morceau de code mort
herbelin
2006-07-07
Correction bug 1172 + correction en passant de la taille des paramètres de f...
herbelin
2005-02-18
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-12
Ajout Print Canonical Structures
herbelin
2004-11-19
Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE
herbelin
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2004-06-25
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2003-06-10
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq
2001-11-05
GROS COMMIT:
barras
2001-10-16
Nettoyage Recordobj et conséquences
herbelin
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-03-15
entetes
filliatr
2001-02-05
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2000-12-19
Export fonction testant si un inductive est un record
herbelin
2000-12-12
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-11-02
suppression des (* open Generic *)
filliatr
2000-09-10
Correction pour make doc
herbelin
2000-09-10
Ajout d'un LetIn primitif.
herbelin
2000-01-11
Ajout de Record
herbelin
1999-12-03
- global_reference traite des variables
filliatr
1999-11-24
Versions initiales
herbelin
[prev]