aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.mli
AgeCommit message (Expand)Author
2003-09-23Fonctions utilesherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2002-12-19Petit netoyage dans libcoq
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2001-11-29reparation de Locatebarras
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-05GROS COMMIT:barras