4 files changed, 65 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"
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 528d6434c..7f3743900 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -194,6 +194,14 @@ let is_unknown = function
   | Unknown -> true
   | Letter | IdentSep | IdentPart | Symbol -> false
 
+let is_ident_part = function
+  | IdentPart -> true
+  | Letter | IdentSep | Symbol | Unknown -> false
+
+let is_ident_sep = function
+  | IdentSep -> true
+  | Letter | IdentPart | Symbol | Unknown -> false
+
 let ident_refutation s =
   if s = ".." then None else try
     let j, n = next_utf8 s 0 in
@@ -227,6 +235,26 @@ let lowercase_first_char s =
   let j, n = next_utf8 s 0 in
   utf8_of_unicode (lowercase_unicode n)
 
+let split_at_first_letter s =
+  let n, v = next_utf8 s 0 in
+  if ((* optim *) n = 1 && s.[0] != '_') || not (is_ident_sep (classify v)) then None
+  else begin
+    let n = ref n in
+    let p = ref 0 in
+    while !n < String.length s &&
+          let n', v = next_utf8 s !n in
+          p := n';
+          (* Test if not letter *)
+          ((* optim *) n' = 1 && (s.[!n] = '_' || s.[!n] = '\''))
+          || let st = classify v in
+             is_ident_sep st || is_ident_part st
+    do n := !n + !p
+    done;
+    let s1 = String.sub s 0 !n in
+    let s2 = String.sub s !n (String.length s - !n) in
+    Some (s1,s2)
+  end
+
 (** For extraction, we need to encode unicode character into ascii ones *)
 
 let is_basic_ascii s =
diff --git a/lib/unicode.mli b/lib/unicode.mli
index a608d5f02..49b844493 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -30,6 +30,10 @@ val is_unknown : status -> bool
     @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string
 
+(** Split a string supposed to be an ident at the first letter;
+    as an optimization, return None if the first character is a letter *)
+val split_at_first_letter : string -> (string * string) option
+
 (** Return [true] if all UTF-8 characters in the input string are just plain
     ASCII characters. Returns [false] otherwise. *)
 val is_basic_ascii : string -> bool
diff --git a/test-suite/bugs/closed/5769.v b/test-suite/bugs/closed/5769.v
new file mode 100644
index 000000000..42573aad8
--- /dev/null
+++ b/test-suite/bugs/closed/5769.v
@@ -0,0 +1,20 @@
+(* Check a few naming heuristics based on types *)
+(* was buggy for types names _something *)
+
+Inductive _foo :=.
+Lemma bob : (sigT (fun x : nat => _foo)) -> _foo.
+destruct 1.
+exact _f.
+Abort.
+
+Inductive _'Foo :=.
+Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo.
+destruct 1.
+exact _'f.
+Abort.
+
+Inductive ____ :=.
+Lemma bob : (sigT (fun x : nat => ____)) -> ____.
+destruct 1.
+exact x0.
+Abort.