Namegen.next_ident_away_in_goal: avoid names of all visible refs

Fix coq#3523

engine/namegen.ml

@@ -62,29 +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
+  match Nametab.locate (qualid_of_ident id) with
+  | exception Not_found -> false
+  | GlobRef.VarRef _ -> false
+  | GlobRef.(IndRef _ | ConstructRef _ | ConstRef _) -> true
 
 let is_constructor id =
   try
@@ -94,10 +76,6 @@ let is_constructor id =
   with Not_found ->
     false
 
-let is_section_variable id =
-  try let _ = Global.lookup_named id in true
-  with Not_found -> false
-
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
@@ -336,7 +314,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 || is_global id 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,14 @@
+Module Foo.
+  Record foor := C { eq : Type }.
+End Foo.
+
+Module bar.
+
+  Goal forall x : Foo.foor, x = x.
+  Proof.
+    intro x.
+    destruct x.
+    revert eq0.
+    exact (fun f => eq_refl (Foo.C f)).
+  Qed.
+End bar.

theories/Floats/FloatLemmas.v

@@ -166,7 +166,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
         intro s0.
         destruct s0.
         unfold shr_1.
-        destruct shr_m; try (simpl; lia).
+        destruct shr_m0; try (simpl; lia).
         - destruct p; unfold Zdigits2, shr_m, digits2_pos; lia.
         - destruct p; unfold Zdigits2, shr_m, digits2_pos; lia.
       }
@@ -286,7 +286,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
         unfold SpecFloat.shr_r, SpecFloat.shr_m.
         intros Hshr_r Hshr_m.
         rewrite Hshr_r, Hshr_m.
-        now destruct shr_s.
+        now destruct shr_s0.
       }
 
       rewrite H0.
@@ -318,7 +318,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
         unfold SpecFloat.shr_r, SpecFloat.shr_m.
         intros Hshr_r Hshr_m.
         rewrite Hshr_r, Hshr_m.
-        now destruct shr_s.
+        now destruct shr_s0.
       }
 
       rewrite Hrne'0.

theories/Reals/Abstract/ConstructiveLimits.v

@@ -72,9 +72,9 @@ Proof.
   - unfold CRminus.
     do 2 rewrite <- (Radd_assoc (CRisRing R)).
     apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr.
-    destruct (CRisRing R). rewrite Radd_comm, <- Radd_assoc.
+    destruct (CRisRing R). rewrite Radd_comm0, <- Radd_assoc0.
     apply CRplus_morph. reflexivity.
-    rewrite Radd_comm. reflexivity.
+    rewrite Radd_comm0. reflexivity.
   - apply (CRle_trans _ _ _ (CRabs_triang _ _)).
     apply (CRle_trans _ (CRplus R (CR_of_Q R (1 # 2*p)) (CR_of_Q R (1 # 2*p)))).
     apply CRplus_le_compat. apply imaj, (le_trans _ _ _ (Nat.le_max_l _ _) H).
@@ -381,18 +381,18 @@ Proof.
   intros. intro r.
   apply (CRplus_lt_compat_r (-l)) in r. rewrite CRplus_opp_r in r.
   destruct (Un_cv_nat_real _ l H0 (A - l) r) as [n H1].
-  apply (H (n+N)%nat).
-  rewrite <- (plus_0_l N). rewrite Nat.add_assoc.
+  apply (H (n+N1)%nat).
+  rewrite <- (plus_0_l N1). rewrite Nat.add_assoc.
   apply Nat.add_le_mono_r. apply le_0_n.
-  specialize (H1 (n+N)%nat). apply (CRplus_lt_reg_r (-l)).
-  assert (n + N >= n)%nat. rewrite <- (plus_0_r n). rewrite <- plus_assoc.
+  specialize (H1 (n+N1)%nat). apply (CRplus_lt_reg_r (-l)).
+  assert (n + N1 >= n)%nat. rewrite <- (plus_0_r n). rewrite <- plus_assoc.
   apply Nat.add_le_mono_l. apply le_0_n. specialize (H1 H2).
-  apply (CRle_lt_trans _ (CRabs R (u (n + N)%nat - l))).
+  apply (CRle_lt_trans _ (CRabs R (u (n + N1)%nat - l))).
   apply CRle_abs. assumption.
 Qed.
 
-Lemma CR_cv_bound_up : forall {R : ConstructiveReals}
-                         (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat),
+Lemma CR_cv_bound_up {R : ConstructiveReals}
+      (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat) :
     (forall n:nat, le N n -> u n <= A)
     -> CR_cv R u l
     -> l <= A.

theories/Reals/Abstract/ConstructiveReals.v

@@ -355,29 +355,29 @@ Qed.
 Lemma CRplus_0_l : forall {R : ConstructiveReals} (x : CRcarrier R),
     0 + x == x.
 Proof.
-  intros. destruct (CRisRing R). apply Radd_0_l.
+  intros. destruct (CRisRing R). apply Radd_0_l0.
 Qed.
 
 Lemma CRplus_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
     x + 0 == x.
 Proof.
   intros. destruct (CRisRing R).
   transitivity (0 + x).
-  apply Radd_comm. apply Radd_0_l.
+  apply Radd_comm0. apply Radd_0_l0.
 Qed.
 
 Lemma CRplus_opp_l : forall {R : ConstructiveReals} (x : CRcarrier R),
     - x + x == 0.
 Proof.
   intros. destruct (CRisRing R).
   transitivity (x + - x).
-  apply Radd_comm. apply Ropp_def.
+  apply Radd_comm0. apply Ropp_def0.
 Qed.
 
 Lemma CRplus_opp_r : forall {R : ConstructiveReals} (x : CRcarrier R),
     x + - x == 0.
 Proof.
-  intros. destruct (CRisRing R). apply Ropp_def.
+  intros. destruct (CRisRing R). apply Ropp_def0.
 Qed.
 
 Lemma CRopp_0 : forall {R : ConstructiveReals},
@@ -391,23 +391,23 @@ Lemma CRplus_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R
     r1 < r2 -> r1 + r < r2 + r.
 Proof.
   intros. destruct (CRisRing R).
-  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _)
+  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm0 _ _)
                      (CRplus R r2 r) (CRplus R r2 r)).
   apply CReq_refl.
   apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)).
-  apply Radd_comm. apply CRplus_lt_compat_l. exact H.
+  apply Radd_comm0. apply CRplus_lt_compat_l. exact H.
 Qed.
 
 Lemma CRplus_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
     r1 + r < r2 + r -> r1 < r2.
 Proof.
   intros. destruct (CRisRing R).
-  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _)
+  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm0 _ _)
                      (CRplus R r2 r) (CRplus R r2 r)) in H.
   2: apply CReq_refl.
   apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)) in H.
   apply CRplus_lt_reg_l in H. exact H.
-  apply Radd_comm.
+  apply Radd_comm0.
 Qed.
 
 Lemma CRplus_le_compat_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
@@ -476,22 +476,22 @@ Lemma CRplus_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
     r + r1 == r + r2 -> r1 == r2.
 Proof.
   intros.
-  destruct (CRisRingExt R). clear Rmul_ext Ropp_ext.
-  pose proof (Radd_ext
+  destruct (CRisRingExt R). clear Rmul_ext0 Ropp_ext0.
+  pose proof (Radd_ext0
                 (CRopp R r) (CRopp R r) (CReq_refl _)
                 _ _ H).
   destruct (CRisRing R).
   apply (CReq_trans r1) in H0.
   apply (CReq_trans _ _ _ H0).
   transitivity ((- r + r) + r2).
-  apply Radd_assoc. transitivity (0 + r2).
-  apply Radd_ext. apply CRplus_opp_l. apply CReq_refl.
-  apply Radd_0_l. apply CReq_sym.
+  apply Radd_assoc0. transitivity (0 + r2).
+  apply Radd_ext0. apply CRplus_opp_l. apply CReq_refl.
+  apply Radd_0_l0. apply CReq_sym.
   transitivity (- r + r + r1).
-  apply Radd_assoc.
+  apply Radd_assoc0.
   transitivity (0 + r1).
-  apply Radd_ext. apply CRplus_opp_l. apply CReq_refl.
-  apply Radd_0_l.
+  apply Radd_ext0. apply CRplus_opp_l. apply CReq_refl.
+  apply Radd_0_l0.
 Qed.
 
 Lemma CRplus_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
@@ -590,14 +590,14 @@ Lemma CRopp_gt_lt_contravar
 Proof.
   intros. apply (CRplus_lt_reg_l R r1).
   destruct (CRisRing R).
-  apply (CRle_lt_trans _ 0). apply Ropp_def.
+  apply (CRle_lt_trans _ 0). apply Ropp_def0.
   apply (CRplus_lt_compat_l R (CRopp R r2)) in H.
   apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)).
   apply (CRle_trans _ (CRplus R r2 (CRopp R r2))).
-  destruct (Ropp_def r2). exact H0.
-  destruct (Radd_comm r2 (CRopp R r2)). exact H1.
+  destruct (Ropp_def0 r2). exact H0.
+  destruct (Radd_comm0 r2 (CRopp R r2)). exact H1.
   apply (CRlt_le_trans _ _ _ H).
-  destruct (Radd_comm r1 (CRopp R r2)). exact H0.
+  destruct (Radd_comm0 r1 (CRopp R r2)). exact H0.
 Qed.
 
 Lemma CRopp_lt_cancel : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
@@ -623,31 +623,31 @@ Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
 Proof.
   intros. destruct (CRisRing R), (CRisRingExt R).
   apply (CRplus_eq_reg_l (CRplus R r1 r2)).
-  transitivity (CR_of_Q R 0). apply Ropp_def.
+  transitivity (CR_of_Q R 0). apply Ropp_def0.
   transitivity (r2 + r1 + (-r1 + -r2)).
   transitivity (r2 + (r1 + (-r1 + -r2))).
   transitivity (r2 + - r2).
-  apply CReq_sym. apply Ropp_def. apply Radd_ext.
+  apply CReq_sym. apply Ropp_def0. apply Radd_ext0.
   apply CReq_refl.
   transitivity (0 + - r2).
-  apply CReq_sym, Radd_0_l.
+  apply CReq_sym, Radd_0_l0.
   transitivity (r1 + - r1 + - r2).
-  apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def.
-  apply CReq_sym, Radd_assoc. apply Radd_assoc.
-  apply Radd_ext. 2: apply CReq_refl. apply Radd_comm.
+  apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, Ropp_def0.
+  apply CReq_sym, Radd_assoc0. apply Radd_assoc0.
+  apply Radd_ext0. 2: apply CReq_refl. apply Radd_comm0.
 Qed.
 
 Lemma CRmult_1_l : forall {R : ConstructiveReals} (r : CRcarrier R),
     1 * r == r.
 Proof.
-  intros. destruct (CRisRing R). apply Rmul_1_l.
+  intros. destruct (CRisRing R). apply Rmul_1_l0.
 Qed.
 
 Lemma CRmult_1_r : forall {R : ConstructiveReals} (x : CRcarrier R),
     x * 1 == x.
 Proof.
   intros. destruct (CRisRing R). transitivity (CRmult R 1 x).
-  apply Rmul_comm. apply Rmul_1_l.
+  apply Rmul_comm0. apply Rmul_1_l0.
 Qed.
 
 Lemma CRmult_assoc : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
@@ -667,14 +667,14 @@ Lemma CRmult_plus_distr_l : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier
 Proof.
   intros. destruct (CRisRing R).
   transitivity ((r2 + r3) * r1).
-  apply Rmul_comm.
+  apply Rmul_comm0.
   transitivity ((r2 * r1) + (r3 * r1)).
-  apply Rdistr_l.
+  apply Rdistr_l0.
   transitivity ((r1 * r2) + (r3 * r1)).
-  destruct (CRisRingExt R). apply Radd_ext.
-  apply Rmul_comm. apply CReq_refl.
-  destruct (CRisRingExt R). apply Radd_ext.
-  apply CReq_refl. apply Rmul_comm.
+  destruct (CRisRingExt R). apply Radd_ext0.
+  apply Rmul_comm0. apply CReq_refl.
+  destruct (CRisRingExt R). apply Radd_ext0.
+  apply CReq_refl. apply Rmul_comm0.
 Qed.
 
 Lemma CRmult_plus_distr_r : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
@@ -698,7 +698,7 @@ Lemma CRmult_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
 Proof.
   intros. apply CRzero_double.
   transitivity (x * (0 + 0)).
-  destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl.
+  destruct (CRisRingExt R). apply Rmul_ext0. apply CReq_refl.
   apply CReq_sym, CRplus_0_r.
   destruct (CRisRing R). apply CRmult_plus_distr_l.
 Qed.
@@ -713,13 +713,13 @@ Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
     - (r1 * r2) == r1 * (- r2).
 Proof.
   intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)).
-  destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def.
+  destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def0.
   transitivity (r1 * (r2 + - r2)).
   2: apply CRmult_plus_distr_l.
   transitivity (r1 * 0).
   apply CReq_sym, CRmult_0_r.
-  destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl.
-  apply CReq_sym, Ropp_def.
+  destruct (CRisRingExt R). apply Rmul_ext0. apply CReq_refl.
+  apply CReq_sym, Ropp_def0.
 Qed.
 
 Lemma CRopp_mult_distr_l : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
@@ -751,7 +751,7 @@ Proof.
   apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1.
   destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2.
   destruct (CRisRing R).
-  destruct (Rdistr_l r2 (CRopp R r1) r). exact H2.
+  destruct (Rdistr_l0 r2 (CRopp R r1) r). exact H2.
   apply CRplus_le_compat_l. destruct (CRopp_mult_distr_l r1 r).
   exact H1.
 Qed.