diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/namegen.ml | 14 |
2 files changed, 14 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 9055dcc86b..96e4b6acce 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -31,7 +31,7 @@ open Environ (** {6 Evars} *) type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) +(** Existential variables. *) val string_of_existential : evar -> string diff --git a/engine/namegen.ml b/engine/namegen.ml index 1dd29e6eae..2e62b89011 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -43,6 +43,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string let default_dependent_ident = Id.of_string "x" +let default_generated_non_letter_string = "x" + (**********************************************************************) (* Globality of identifiers *) @@ -107,7 +109,17 @@ let head_name sigma c = (* Find the head constant of a constr if any *) hdrec c let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) + let s = Id.to_string id in + match Unicode.split_at_first_letter s with + | None -> + (* General case: nat -> n *) + Unicode.lowercase_first_char s + | Some (s,s') -> + if String.length s' = 0 then + (* No letter, e.g. __, or __'_, etc. *) + default_generated_non_letter_string + else + s ^ Unicode.lowercase_first_char s' let sort_hdchar = function | Prop(_) -> "P" |