aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.mli
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* COMMENT: was added to "Nameops.increment_suffix".Gravatar Matej Kosik2016-10-19
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Updating headers.Gravatar herbelin2012-08-08
* 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