aboutsummaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
AgeCommit message (Expand)Author
2003-11-04Extension de zarithherbelin
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...herbelin
2003-10-21Optimisation de gen_constant_in_modulesherbelin
2003-10-14identityT = identityherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les tact...herbelin
2003-09-12open superfluherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-19Restructuration des procédures de filtrageherbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin