[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

1 files changed, 32 insertions, 32 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 3bcec3001..150be040f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -220,10 +220,10 @@ let remove_delimiters scope =
        with Not_found ->
          assert false (* A delimiter for scope [scope] should exist *)
 
-let find_delimiters_scope loc key =
+let find_delimiters_scope ?loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
-    user_err ~loc ~hdr:"find_delimiters"
+    user_err ?loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
@@ -291,7 +291,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 type required_module = full_path * string list
 
 type 'a prim_token_interpreter =
-    Loc.t -> 'a -> glob_constr
+    ?loc:Loc.t -> 'a -> glob_constr
 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
@@ -299,7 +299,7 @@ type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
-    Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+    ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
 
 let prim_token_interpreter_tab =
   (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -309,7 +309,7 @@ let add_prim_token_interpreter sc interp =
     let cont = Hashtbl.find prim_token_interpreter_tab sc in
     Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
   with Not_found ->
-    let cont = (fun _loc _p -> raise Not_found) in
+    let cont = (fun ?loc _p -> raise Not_found) in
     Hashtbl.add prim_token_interpreter_tab sc (interp cont)
 
 let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
@@ -325,22 +325,22 @@ let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let delay dir int loc x = (dir, (fun () -> int loc x))
+let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+    (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+    (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
     (patl, (fun r -> mkString (uninterp r)), inpat)
 
-let check_required_module loc sc (sp,d) =
+let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ~loc ~hdr:"prim_token_interpreter"
+    user_err ?loc ~hdr:"prim_token_interpreter"
     (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
@@ -445,23 +445,23 @@ let notation_of_prim_token = function
   | Numeral n -> "- "^(to_string (neg n))
   | String _ -> raise Not_found
 
-let find_prim_token g loc p sc =
+let find_prim_token ?loc g p sc =
   (* Try for a user-defined numerical notation *)
   try
     let (_,c),df = find_notation (notation_of_prim_token p) sc in
-    g (Notation_ops.glob_constr_of_notation_constr loc c),df
+    g (Notation_ops.glob_constr_of_notation_constr ?loc c),df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
-  check_required_module loc sc spdir;
+  let (spdir,interp) = (Hashtbl.find prim_token_interpreter_tab sc) ?loc p in
+  check_required_module ?loc sc spdir;
   g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
 
-let interp_prim_token_gen g loc p local_scopes =
+let interp_prim_token_gen g ?loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
-  try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
+  try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
   with Not_found ->
-    user_err ~loc ~hdr:"interp_prim_token"
+    user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
@@ -480,14 +480,14 @@ let rec rcp_of_glob looked_for gt = Loc.map (function
   | _ -> raise Not_found
   ) gt
 
-let interp_prim_token_cases_pattern_expr loc looked_for p =
-  interp_prim_token_gen (rcp_of_glob looked_for) loc p
+let interp_prim_token_cases_pattern_expr ?loc looked_for p =
+  interp_prim_token_gen (rcp_of_glob looked_for) ?loc p
 
-let interp_notation loc ntn local_scopes =
+let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
-    user_err ~loc 
+    user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
@@ -541,7 +541,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true
+    try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
     with Not_found -> false in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -823,7 +823,7 @@ let pr_scope_classes sc =
 
 let pr_notation_info prglob ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++
-  prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
+  prglob (Notation_ops.glob_constr_of_notation_constr c)
 
 let pr_named_scope prglob scope sc =
  (if String.equal scope default_scope then
@@ -891,25 +891,25 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
       Some (ntn,sc,ref)
   | _ -> None
 
-let error_ambiguous_notation loc _ntn =
-  user_err ~loc  (str "Ambiguous notation.")
+let error_ambiguous_notation ?loc _ntn =
+  user_err ?loc (str "Ambiguous notation.")
 
-let error_notation_not_reference loc ntn =
-  user_err ~loc 
+let error_notation_not_reference ?loc ntn =
+  user_err ?loc 
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference loc test ntn sc =
+let interp_notation_as_global_reference ?loc test ntn sc =
   let scopes = match sc with
   | Some sc ->
-      let scope = find_scope (find_delimiters_scope Loc.ghost sc) in
+      let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
-  | [] -> error_notation_not_reference loc ntn
+  | [] -> error_notation_not_reference ?loc ntn
   | refs ->
       let f (ntn,sc,ref) =
         let def = find_default ntn !scope_stack in
@@ -919,8 +919,8 @@ let interp_notation_as_global_reference loc test ntn sc =
       in
       match List.filter f refs with
       | [_,_,ref] -> ref
-      | [] -> error_notation_not_reference loc ntn
-      | _ -> error_ambiguous_notation loc ntn
+      | [] -> error_notation_not_reference ?loc ntn
+      | _ -> error_ambiguous_notation ?loc ntn
 
 let locate_notation prglob ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in