Namegen.next_ident_away_in_goal: don't avoid names of nonlocal refs

Fix coq#3523

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

@@ -0,0 +1,4 @@
+- **Changed:** Name generation does not avoid names of references
+  except for those from the current module and its ancestors (`#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,27 +62,29 @@ 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
+let is_local_modpath mp =
+  let rec is_prefixed cur =
+    ModPath.equal mp cur ||
+    match cur with
+    | MPbound _ | MPfile _ -> false
+    | MPdot (cur,_) -> is_prefixed cur
+  in
+  let cur = Lib.current_mp () in
+  is_prefixed cur
+
+let is_local_ref = let open GlobRef in
+  function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
-      let mp = MutInd.modpath kn in is_imported_modpath mp
+    let mp = MutInd.modpath kn in is_local_modpath mp
   | ConstRef kn ->
-      let mp = Constant.modpath kn in is_imported_modpath mp
+    let mp = Constant.modpath kn in is_local_modpath mp
 
-let is_global id =
+let is_local id =
   try
     let ref = Nametab.locate (qualid_of_ident id) in
-    not (is_imported_ref ref)
+    is_local_ref ref
   with Not_found ->
     false
 
@@ -94,10 +96,6 @@ let is_constructor id =
   with Not_found ->
     false
 
-let is_section_variable env id =
-  try let _ = Environ.lookup_named id env in true
-  with Not_found -> false
-
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
@@ -336,7 +334,7 @@ let next_name_away_in_cases_pattern sigma env_t na avoid =
 
 let next_ident_away_in_goal env 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 env id)) in
+  let bad id = Id.Set.mem id avoid || is_local id in
   next_ident_away_from id bad
 
 let next_name_away_in_goal env na avoid =

test-suite/bugs/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.

theories/FSets/FMapFacts.v

@@ -1877,9 +1877,9 @@ Module OrdProperties (M:S).
   2: auto with map.
   intros; destruct x; destruct y; destruct p.
   rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
-  assert (~ltk (t1,e0) (k,e1)).
+  assert (~ltk (t0,e0) (k,e1)).
   - unfold gtb, O.ltk in *; simpl in *.
-    destruct (E.compare k t1); intuition; try discriminate; ME.order.
+    destruct (E.compare k t0); intuition; try discriminate; ME.order.
   - unfold O.ltk in *; simpl in *; ME.order.
   Qed.
 
@@ -1901,9 +1901,9 @@ Module OrdProperties (M:S).
            rewrite leb_1 in H2.
            destruct y; unfold O.ltk in *; simpl in *.
            rewrite <- elements_mapsto_iff in H1.
-           assert (~E.eq x t0).
+           assert (~E.eq x t).
            ++ contradict H.
-              exists e0; apply MapsTo_1 with t0; auto with ordered_type.
+              exists e0; apply MapsTo_1 with t; auto with ordered_type.
            ++ ME.order.
         -- apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map.
     + intros.
@@ -1919,12 +1919,12 @@ Module OrdProperties (M:S).
   - red; intros a; destruct a.
     rewrite InA_app_iff, InA_cons, 2 filter_InA,
       <-2 elements_mapsto_iff, leb_1, gtb_1,
-      find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+      find_mapsto_iff, (H0 t), <- find_mapsto_iff,
       add_mapsto_iff by auto with map.
     unfold O.eqke, O.ltk; simpl.
-    destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type.
-    + elim H; exists e0; apply MapsTo_1 with t0; auto.
-    + fold (~E.lt t0 x); auto with ordered_type.
+    destruct (E.compare t x); intuition; try fold (~E.eq x t); auto with ordered_type.
+    + elim H; exists e0; apply MapsTo_1 with t; auto.
+    + fold (~E.lt t x); auto with ordered_type.
   Qed.
 
   Lemma elements_Add_Above : forall m m' x e,
@@ -1948,14 +1948,14 @@ Module OrdProperties (M:S).
       * inversion H3.
   - red; intros a; destruct a.
     rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff,
-      find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+      find_mapsto_iff, (H0 t), <- find_mapsto_iff,
       add_mapsto_iff.
     unfold O.eqke; simpl. intuition auto with relations.
-    destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
+    destruct (E.eq_dec x t) as [Heq|Hneq]; auto.
     exfalso.
-    assert (In t0 m).
+    assert (In t m).
     + exists e0; auto.
-    + generalize (H t0 H1).
+    + generalize (H t H1).
       ME.order.
   Qed.
 
@@ -1981,14 +1981,14 @@ Module OrdProperties (M:S).
       * inversion H3.
   - red; intros a; destruct a.
     rewrite InA_cons, <- 2 elements_mapsto_iff,
-      find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+      find_mapsto_iff, (H0 t), <- find_mapsto_iff,
       add_mapsto_iff.
     unfold O.eqke; simpl. intuition auto with relations.
-    destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
+    destruct (E.eq_dec x t) as [Heq|Hneq]; auto.
     exfalso.
-    assert (In t0 m) by
+    assert (In t m) by
       (exists e0; auto).
-    generalize (H t0 H1).
+    generalize (H t H1).
     ME.order.
   Qed.