aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.ml
AgeCommit message (Expand)Author
2003-09-09errorherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-20Extension renommageherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
2003-05-13Orthographe anglaise - typosherbelin
2003-05-13Orthographe anglaiseherbelin
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-07Renommage unicite/unicity pour la v8herbelin
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-12-09Corrections de gestion des univers et modules + meilleure gestions des noms...coq
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2001-12-13compat ocaml 3.03filliatr
2001-11-29reparation de Locatebarras
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-05GROS COMMIT:barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 14:17:31 +0000