aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.ml
AgeCommit message (Expand)Author
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-08-29Canonically renaming fold_map into fold_left_map in library Name.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01Remove a post merge warning.Maxime Dénès
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
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-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-22Less "Coq" strings everywhereletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (library)ppedrot
2012-11-13More monomorphizationsppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
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
2006-04-24Changement anomaly en failwith dans out_name pour utilisation par map_succeedherbelin
2004-10-12Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...herbelin
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-09-09errorherbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-05-20Extension renommageherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
2003-05-13Orthographe anglaise - typosherbelin
2003-05-13Orthographe anglaiseherbelin
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-07Renommage unicite/unicity pour la v8herbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:57:35 +0000