diff --git a/engine/namegen.ml b/engine/namegen.ml index 75bf2a84892dc..cd4492974c8b4 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -80,7 +80,7 @@ let is_imported_ref = let open GlobRef in function let mp = Constant.modpath kn in is_imported_modpath mp let locate id = - match fst (Nametab.locate_extended_nowarn (qualid_of_ident id)) with + match Nametab.locate_extended_nowarn (qualid_of_ident id) with | TrueGlobal r -> r | Abbrev _ -> raise Not_found diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7944d41c401ff..66908e93d7f48 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1336,12 +1336,12 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let intern_qualid_for_pattern test_global intern_not qid pats = match Nametab.locate_extended_nowarn qid with - | TrueGlobal g, depr -> + | TrueGlobal g as xref -> test_global g; - depr |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (TrueGlobal g)); + Nametab.is_deprecated_xref xref |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (TrueGlobal g)); dump_extended_global qid.loc (TrueGlobal g); (g, false, Some [], pats) - | Abbrev kn, depr -> + | Abbrev kn as xref -> let filter (vars,a) = match a with | NRef (g,_) -> @@ -1365,7 +1365,8 @@ let intern_qualid_for_pattern test_global intern_not qid pats = | _ -> None in match Abbreviation.search_filtered_abbreviation filter kn with | Some (g, pats1, pats2) -> - depr |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (Abbrev kn)); + Nametab.is_deprecated_xref xref + |> Option.iter (fun depr -> Nametab.warn_deprecated_xref ?loc:qid.loc depr (Abbrev kn)); dump_extended_global qid.loc (Abbrev kn); (g, true, pats1, pats2) | None -> raise Not_found diff --git a/library/nametab.ml b/library/nametab.ml index a8f13d5bd2576..20a69b5637454 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -596,12 +596,12 @@ let is_deprecated_xref xref = Globnames.ExtRefMap.find_opt xref !the_globdeprtab let locate_extended_nowarn qid = let xref = ExtRefTab.locate qid !the_ccitab in - let depr = is_deprecated_xref xref in - xref, depr + xref (* This should be used when abbreviations are allowed *) let locate_extended qid = - let xref, depr = locate_extended_nowarn qid in + let xref = locate_extended_nowarn qid in + let depr = is_deprecated_xref xref in let () = depr |> Option.iter (fun depr -> warn_deprecated_xref ?loc:qid.loc depr xref) in diff --git a/library/nametab.mli b/library/nametab.mli index 18d9cd1ffee1c..bc353bdb30731 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -135,7 +135,7 @@ val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t val locate_universe : qualid -> Univ.UGlobal.t -val locate_extended_nowarn : qualid -> Globnames.extended_global_reference * Deprecation.t option +val locate_extended_nowarn : qualid -> Globnames.extended_global_reference (** Remove the binding to an abbreviation *)