index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
recordops.ml
Commit message (
Expand
)
Author
Age
...
*
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-06-29
*
added products and sorts as possible heads for canonical structures
corbinea
2008-02-19
*
Added default canonical structures (see example in test-suite)
corbinea
2008-02-14
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Wish #1187 granted (support for canonical structures that are records
herbelin
2006-09-23
*
Morceau de code mort
herbelin
2006-08-24
*
Correction bug 1172 + correction en passant de la taille des paramètres de f...
herbelin
2006-07-07
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
Types inductifs parametriques
mohring
2005-11-02
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
HUGE COMMIT
sacerdot
2005-01-03
*
Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE
herbelin
2004-11-19
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
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
*
Déclaration des record au chargement (ce n'est pas une question de visibilit...
herbelin
2004-04-05
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
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
*
Les tables de coercions ne doivent pas survivre aux sections
herbelin
2001-07-06
*
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
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
methode export
filliatr
2000-11-15
*
Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...
herbelin
2000-11-10
*
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
*
MAJ ocaml 2.99 (espaces dans la syntaxe des cast)
herbelin
2000-01-26
*
Ajout de Record
herbelin
2000-01-11
*
changement type add_anonymous_leaf
filliatr
1999-12-05
*
portage Astterm (partiellement)
filliatr
1999-11-29
*
fin Recordops, et debut Evarutil
filliatr
1999-11-27
*
Maintenant compilable
herbelin
1999-11-26
*
module Classops; ajout de fonctions dans Declare en consequence
filliatr
1999-11-26
*
Des progres dans l'integration
herbelin
1999-11-25
*
Versions initiales
herbelin
1999-11-24
[prev]