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
*
Ajout nat_path et find_reference
herbelin
2006-02-04
*
exporting the global reference to the inductive " \/ " in coqlib and
bertot
2006-01-25
*
Ajout booléens; nettoyage
herbelin
2005-12-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
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