index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
record.mli
Commit message (
Expand
)
Author
Age
*
Les records déclarés avec Record ne peuvent plus être récursifs (le
aspiwack
2009-01-19
*
DISCLAIMER
puech
2009-01-17
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
Fixed bug #2006 (type constraint on Record was not taken into account) +
herbelin
2008-11-23
*
Fix mixup between Record, Structure and Class by adding a new variant for
msozeau
2008-11-10
*
More factorization of inductive/record and typeclasses: move class
msozeau
2008-11-09
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
Nouvelle syntaxe pour écrire des records (co)inductifs :
aspiwack
2008-11-05
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
Fix bugs that were reopened due to the change of setoid
msozeau
2008-03-08
*
Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...
msozeau
2007-12-31
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Nouvelle en-tête
herbelin
2004-07-16
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Utilisation des de Bruijn pour la constructions des records et de leur projec...
herbelin
2002-05-13
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
entetes
filliatr
2001-03-15
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Ajout de Record
herbelin
2000-01-11
*
- global_reference traite des variables
filliatr
1999-12-03
*
Version initiale
herbelin
1999-12-02