Namegen.nex_ident_away_in_goal: don't avoid names of globrefs

Fix coq#3523

doc/changelog/04-tactics/15071-namegen-no-glob.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  Name generation does not avoid names of references from the current file
+  (`#15071 <https://github.com/coq/coq/pull/15071>`_,
+  fixes `#3523 <https://github.com/coq/coq/issues/3523>`_,
+  by Gaëtan Gilbert).

engine/namegen.ml

@@ -62,41 +62,11 @@ let default_generated_non_letter_string = "x"
 (**********************************************************************)
 (* Globality of identifiers *)
 
-let is_imported_modpath = function
-  | MPfile dp ->
-    let rec find_prefix = function
-      |MPfile dp1 -> not (DirPath.equal dp1 dp)
-      |MPdot(mp,_) -> find_prefix mp
-      |MPbound(_) -> false
-    in find_prefix (Lib.current_mp ())
-  | _ -> false
-
-let is_imported_ref = let open GlobRef in function
-  | VarRef _ -> false
-  | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) ->
-      let mp = MutInd.modpath kn in is_imported_modpath mp
-  | ConstRef kn ->
-      let mp = Constant.modpath kn in is_imported_modpath mp
-
-let is_global id =
-  try
-    let ref = Nametab.locate (qualid_of_ident id) in
-    not (is_imported_ref ref)
-  with Not_found ->
-    false
-
 let is_constructor id =
-  try
-    match Nametab.locate (qualid_of_ident id) with
-      | GlobRef.ConstructRef _ -> true
-      | _ -> false
-  with Not_found ->
-    false
-
-let is_section_variable id =
-  try let _ = Global.lookup_named id in true
-  with Not_found -> false
+  match Nametab.locate (qualid_of_ident id) with
+  | GlobRef.ConstructRef _ -> true
+  | _ -> false
+  | exception Not_found -> false
 
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
@@ -322,7 +292,8 @@ let next_name_away_in_cases_pattern sigma env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
   let visible = visible_ids sigma env_t in
   let bad id = Id.Set.mem id avoid || is_constructor id
-                                    || Id.Set.mem id visible in
+               || Id.Set.mem id visible
+  in
   next_ident_away_from id bad
 
 (* 2- Looks for a fresh name for introduction in goal *)
@@ -336,7 +307,7 @@ let next_name_away_in_cases_pattern sigma env_t na avoid =
 
 let next_ident_away_in_goal id avoid =
   let id = if Id.Set.mem id avoid then restart_subscript id else id in
-  let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in
+  let bad id = Id.Set.mem id avoid in
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =

test-suite/bugs/closed/bug_3523.v

@@ -0,0 +1,15 @@
+Module Foo.
+  Record foor := C { foof : Type }.
+End Foo.
+
+Module bar.
+  Import Foo.
+
+  Goal forall x : foor, x = x.
+  Proof.
+    intro x.
+    destruct x.
+    revert foof.
+    exact (fun f => eq_refl (C f)).
+  Qed.
+End bar.