aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.mli
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* 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