aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.ml
AgeCommit message (Expand)Author
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