aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.mli
Commit message (Expand)AuthorAge
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* name_app accessible a tous dans NameopsGravatar herbelin2003-12-19
* Fonctions utilesGravatar herbelin2003-09-23
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* 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
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* 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-23 11:09:02 +0000