index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
coqlib.ml
Commit message (
Expand
)
Author
Age
*
Nouvelle en-tête
herbelin
2004-07-16
*
Branchement EmptyT, UnitT, IT vers leur equivalent dans Set
herbelin
2004-03-11
*
Extension de zarith
herbelin
2003-11-04
*
Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...
herbelin
2003-11-01
*
Optimisation de gen_constant_in_modules
herbelin
2003-10-21
*
identityT = identity
herbelin
2003-10-14
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
open superflu
herbelin
2003-09-12
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
*
Mise en place d'un traducteur de noms v7->v8
herbelin
2003-03-31
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
eq fusionne avec eqT et devient par défaut sur Type,
herbelin
2003-03-29
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14