aboutsummaryrefslogtreecommitdiff
path: root/library/nameops.ml
AgeCommit message (Collapse)Author
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
2017-08-29Canonically renaming fold_map into fold_left_map in library Name.Hugo Herbelin
Also adding fold_right_map by consistency.
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
This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`.
2016-10-19COMMENT: was added to "Nameops.increment_suffix".Matej Kosik
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
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
For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read.
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
Indeed, the name of a bound variable was lost when unifying under a Prod in evarconv. The error message for "Unable to satisfy the following constraints" is still to be improved though.
2015-01-12Update headers.Maxime Dénès
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Less "Coq" strings everywhereletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of Labelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of dir_pathppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (library)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15993 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Correction bug #1041 (double cause : non évitement des noms existants enherbelin
cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Ajout combinateurs option_fold_left et name_fold_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Changement anomaly en failwith dans out_name pour utilisation par map_succeedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8727 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12Prise en compte dans cut_ident des idents de la form _23 qui sont ↵herbelin
officiellement autorisés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6205 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19name_app accessible a tous dans Nameopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Fonctions utilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4460 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4328 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Extension renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4037 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Orthographe anglaise - typosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4007 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Orthographe anglaiseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4006 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ↵herbelin
Rlt_sym, Rle_sym; utilisation de la terminologie 'commutative' plutôt que 'symétrie' pour les opérateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3972 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Renommage unicite/unicity pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:25:23 +0000