Nametab.located_extended_nowarn: don't return deprecation info

It can be looked up separately

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
 

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

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

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 *)