From 40260a31cd197f655e6d3e0570a88d96fc1a9cac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Oct 2017 15:37:36 +0200 Subject: Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). --- engine/namegen.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'engine/namegen.ml') 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" -- cgit v1.2.3