diff --git a/doc/changelog/04-tactics/15071-namegen-no-glob.rst b/doc/changelog/04-tactics/15071-namegen-no-glob.rst new file mode 100644 index 0000000000000..bc0eab4b32450 --- /dev/null +++ b/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 + `_, fixes `#3523 + `_, by Gaëtan Gilbert). diff --git a/engine/namegen.ml b/engine/namegen.ml index b2e48041d1143..0e64a8aa5b241 100644 --- a/engine/namegen.ml +++ b/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 = diff --git a/test-suite/bugs/bug_3523.v b/test-suite/bugs/bug_3523.v new file mode 100644 index 0000000000000..96c20eaf4544b --- /dev/null +++ b/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. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 1ef5aacc681fb..e250755788d23 100644 --- a/theories/FSets/FMapFacts.v +++ b/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.