aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.ml
Commit message (Expand)AuthorAge
* Fonctions utilesGravatar herbelin2003-09-23
* errorGravatar herbelin2003-09-09
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Extension renommageGravatar herbelin2003-05-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
* Orthographe anglaise - typosGravatar herbelin2003-05-13
* Orthographe anglaiseGravatar herbelin2003-05-13
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* Renommage unicite/unicity pour la v8Gravatar herbelin2003-04-07
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* Petit netoyage dans libGravatar coq2002-12-19
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* compat ocaml 3.03Gravatar filliatr2001-12-13
* reparation de LocateGravatar barras2001-11-29
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 04:21:45 +0000