From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 library/nametab.ml | 50 ++++++++++++++++++++++++--------------------------
 1 file changed, 24 insertions(+), 26 deletions(-)

(limited to 'library/nametab.ml')

diff --git a/library/nametab.ml b/library/nametab.ml
index 2046bf75..a3b3ca6e 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
 
 exception GlobalizationError of qualid
 
-let error_global_not_found {CAst.loc;v} =
-  Loc.raise ?loc (GlobalizationError v)
+let error_global_not_found qid =
+  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
 
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
@@ -69,7 +69,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
@@ -220,7 +220,7 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid ctx uname tab =
+let shortest_qualid ?loc ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Id.Set.mem id ctx in
   let rec find_uname pos dir tree =
@@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab =
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
-    make_qualid (DirPath.make found_dir) id
+    make_qualid ?loc (DirPath.make found_dir) id
 
 let push_node node l =
   match node with
@@ -432,7 +432,6 @@ let full_name_module qid =
 let locate_section qid =
   match locate_dir qid with
     | DirOpenSection { obj_dir; _ } -> obj_dir
-    | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
 let locate_all qid =
@@ -459,14 +458,13 @@ let global_of_path sp =
 
 let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
-let global ({CAst.loc;v=r} as lr)=
-  let {CAst.loc; v} as qid = qualid_of_reference lr in
-  try match locate_extended v with
+let global qid =
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ?loc ~hdr:"global"
+        user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
-           pr_qualid v)
+           pr_qualid qid)
   with Not_found ->
     error_global_not_found qid
 
@@ -511,40 +509,40 @@ let path_of_universe mp =
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx ref =
+let shortest_qualid_of_global ?loc ctx ref =
   match ref with
-    | VarRef id -> make_qualid DirPath.empty id
+    | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        ExtRefTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef ctx kn =
+let shortest_qualid_of_syndef ?loc ctx kn =
   let sp = path_of_syndef kn in
-    ExtRefTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_module mp =
+let shortest_qualid_of_module ?loc mp =
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
+    DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab
 
-let shortest_qualid_of_modtype kn =
+let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
+    MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe kn =
+let shortest_qualid_of_universe ?loc kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
     if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
-let global_inductive ({CAst.loc; v=r} as lr) =
-  match global lr with
+let global_inductive qid =
+  match global qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc ~hdr:"global_inductive"
-        (pr_reference lr ++ spc () ++ str "is not an inductive type")
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not an inductive type")
 
 (********************************************************************)
 
-- 
cgit v1.2.3