aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
Commit message (Expand)AuthorAge
* 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