diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-04 15:37:36 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-05 08:38:45 +0200 |
commit | 40260a31cd197f655e6d3e0570a88d96fc1a9cac (patch) | |
tree | 0d0618bda35573e674b55a86364a5e39bf054442 /engine/namegen.ml | |
parent | 526791d917f9b0804376eae02a462a3b32dd7cba (diff) |
Fixing BZ#5769 (variable of type "_something" was named after invalid "_").
Diffstat (limited to 'engine/namegen.ml')
-rw-r--r-- | engine/namegen.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index a75fe721f..6c6a54127 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" |