aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
Commit message (Expand)AuthorAge
* Extension de zarithGravatar herbelin2003-11-04
* Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...Gravatar herbelin2003-11-01
* Optimisation de gen_constant_in_modulesGravatar herbelin2003-10-21
* identityT = identityGravatar herbelin2003-10-14
* identity est equivalent sur Type (sauf sans argument)Gravatar herbelin2003-10-10
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* open superfluGravatar herbelin2003-09-12
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14