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/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.

theories/FSets/FMapFacts.v

@@ -1864,9 +1864,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.
 
@@ -1886,9 +1886,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.
@@ -1904,12 +1904,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,
@@ -1929,14 +1929,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.
-  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.
 
@@ -1958,14 +1958,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.
-  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.
 

theories/setoid_ring/Ncring_polynom.v

@@ -218,13 +218,13 @@ Definition Psub(P P':Pol):= P ++ (--P').
  Proof.
   intros l P i n Q;unfold mkPX.
   destruct P;try (simpl;reflexivity).
-  assert (Hh := ring_morphism_eq  c 0). 
+  assert (Hh := ring_morphism_eq  c 0).
   simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
   intros.
   rewrite Hh. rewrite ring_morphism0.
   rsimpl. apply Ceqb_eq. trivial.
   destruct (Pos.compare_spec i p).
-  assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
+  assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl.
   rewrite Hh. 
   rewrite Pphi0. rsimpl. rewrite Pos.add_comm. rewrite pow_pos_add;rsimpl.
   subst;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
@@ -255,7 +255,7 @@ Ltac Esimpl :=
  Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
  Proof.
   induction P; simpl; intros; Esimpl; try reflexivity.
- rewrite IHP2. rsimpl. 
+ rewrite IHP2. rsimpl.
 rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) [c]).
 reflexivity.
  Qed.
@@ -339,7 +339,7 @@ rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pos.add_comm in H1h.
 rewrite H1h.  Esimpl2. rewrite pow_pos_add. Esimpl2.
 rewrite Hh; trivial. reflexivity.
 rewrite mkPX_ok. rewrite IHP2. Esimpl2.
-rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) 
+rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0)
                              ([c] * pow_pos (nth 0 k l) n)).
 reflexivity.  assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c  0); 
  intros; simpl.