aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.mli
AgeCommit message (Expand)Author
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-08-29Canonically renaming fold_map into fold_left_map in library Name.Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2016-10-19COMMENT: was added to "Nameops.increment_suffix".Matej Kosik
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2013-08-22Less "Coq" strings everywhereletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2006-12-12Correction bug #1041 (double cause : non évitement des noms existants enherbelin
2006-10-09Ajout combinateurs option_fold_left et name_fold_mapherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-07-16Nouvelle en-têteherbelin
2003-12-19name_app accessible a tous dans Nameopsherbelin
2003-09-23Fonctions utilesherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2002-12-19Petit netoyage dans libcoq
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2001-11-29reparation de Locatebarras
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-05GROS COMMIT:barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:30:12 +0000