[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

11 files changed, 31 insertions, 35 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b9c4c6cc5d..fd454b67e5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -60,8 +60,6 @@ exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
 
-let dl = Loc.ghost
-
 let constr_of_global g = lazy (Universes.constr_of_global g)
 
 (* Some pre declaration of constant we are going to use *)
@@ -88,12 +86,12 @@ let destruct_on c = destruct false None c None None
 
 let destruct_on_using c id =
   destruct false None c
-    (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous];
-               [dl,IntroNaming (IntroIdentifier id)]]))
+    (Some (Loc.tag @@ IntroOrPattern [[Loc.tag @@ IntroNaming IntroAnonymous];
+               [Loc.tag @@ IntroNaming (IntroIdentifier id)]]))
     None
 
 let destruct_on_as c l =
-  destruct false None c (Some (dl,l)) None
+  destruct false None c (Some (Loc.tag l)) None
 
 (* reconstruct the inductive with the correct deBruijn indexes *)
 let mkFullInd (ind,u) n =
@@ -611,8 +609,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                          Proofview.Goal.enter { enter = begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
                             destruct_on_as (EConstr.mkVar freshz)
-                                  (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
-                                    dl,IntroNaming (IntroIdentifier freshz)]])
+                                  (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht);
+                                    Loc.tag @@ IntroNaming (IntroIdentifier freshz)]])
                          end }
                         ]);
 (*
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ffe03bfb75..bdaa3ece6d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -408,7 +408,7 @@ let context poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus =
         pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
-          Vernacexpr.NoInline (Loc.ghost, id))
+          Vernacexpr.NoInline (Loc.tag id))
       in
       let () = uctx := Univ.ContextSet.empty in
 	status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 446afb5787..fbaa094301 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -267,7 +267,7 @@ match local with
     (gr,inst,Lib.is_modtype_strict ())
 
 let interp_assumption evdref env impls bl c =
-  let c = mkCProdN (local_binders_loc bl) bl c in
+  let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
   let ty, impls = interp_type_evars_impls env evdref ~impls c in
   let ty = EConstr.Unsafe.to_constr ty in
   (ty, impls)
@@ -917,7 +917,7 @@ let mkSubset name typ prop =
 	 [| typ; mkLambda (name, typ, prop) |])
 let sigT = Lazy.from_fun build_sigma_type
 
-let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
+let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope l =
@@ -1059,7 +1059,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
-	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
   let def = Typing.e_solve_evars env evdref def in
@@ -1212,7 +1212,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let env = Global.env() in
-    let indexes = search_guard Loc.ghost env indexes fixdecls in
+    let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
@@ -1327,8 +1327,7 @@ let do_program_recursive local p fixkind fixl ntns =
 	Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       in
       let indexes = 
-        Pretyping.search_guard
-          Loc.ghost (Global.env ()) possible_indexes fixdecls in
+        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in
       List.iteri (fun i _ ->
           Inductive.check_fix env
                               ((indexes,i),fixdecls))
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 04841c922e..ed2dd274a7 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -119,6 +119,6 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   in
   match e' with
   | None -> e
-  | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
-  | Some (Some msg, loc) ->
+  | Some (loc, None) -> (fst e, Loc.add_loc (snd e) loc)
+  | Some (loc, Some msg) ->
     (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 370ad7e3b5..9202729cee 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -18,4 +18,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
 
 val explain_exn_default : exn -> Pp.std_ppcmds
 
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 9ba4e46e48..2367177e22 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -379,7 +379,7 @@ requested
               | InType -> recs ^ "t_nodep")
         ) in
         let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
-        let newref = (Loc.ghost,newid) in
+        let newref = Loc.tag newid in
           ((newref,isdep,ind,z)::l1),l2
       in
 	match t with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 993a2c260d..b51792b1e3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -81,7 +81,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
-                search_guard Loc.ghost env
+                search_guard env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 98b2c3729b..a586fe9f27 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = Loc.tag @@ CRef (Ident (Loc.ghost, Id.of_string x),None)
+let inject_var x = Loc.tag @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
 
 let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ea2401b5ce..5e65855ef9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -558,8 +558,7 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-              Pretyping.search_guard
-              Loc.ghost (Global.env())
+              Pretyping.search_guard (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
           List.map_i (fun i _ ->
@@ -674,7 +673,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 	assert(Int.equal (Array.length obls) 0);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
+	       obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
 	       obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
 	       obl_tac = None } |],
 	mkVar n
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 86406dbe56..75f403e339 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -643,7 +643,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   in
   Dumpglob.dump_moddef loc mp "mod";
   if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
-  Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
+  Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -668,7 +668,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
+             (fun export -> vernac_import export [Ident (Loc.tag id)]) export
          ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -683,7 +683,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        Dumpglob.dump_moddef loc mp "mod";
        if_verbose Feedback.msg_info
 	 (str "Module " ++ pr_id id ++ str " is defined");
-       Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
+       Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
          export
 
 let vernac_end_module export (loc,id as lid) =
@@ -715,7 +715,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
+             (fun export -> vernac_import export [Ident (Loc.tag id)]) export
          ) argsexport
 
     | _ :: _ ->
@@ -1176,10 +1176,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   end;
 
   if scopes_specified || clear_scopes_flag then begin
-      let scopes = List.map (Option.map (fun (o,k) -> 
+      let scopes = List.map (Option.map (fun (loc,k) -> 
         try ignore (Notation.find_scope k); k
         with UserError _ ->
-          Notation.find_delimiters_scope o k)) scopes
+          Notation.find_delimiters_scope ~loc k)) scopes
       in
       vernac_arguments_scope locality reference scopes
     end;
@@ -1708,7 +1708,7 @@ let interp_search_about_item env =
   | SearchString (s,sc) ->
       try
 	let ref =
-	  Notation.interp_notation_as_global_reference Loc.ghost
+	  Notation.interp_notation_as_global_reference
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
@@ -2065,15 +2065,15 @@ let interp ?proof ~loc locality poly c =
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
   | VernacProof (None, None) ->
-      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no"
+      Aux_file.record_in_aux_at ~loc "VernacProof" "tac:no using:no"
   | VernacProof (Some tac, None) ->
-      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no";
+      Aux_file.record_in_aux_at ~loc "VernacProof" "tac:yes using:no";
       vernac_set_end_tac tac
   | VernacProof (None, Some l) ->
-      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes";
+      Aux_file.record_in_aux_at ~loc "VernacProof" "tac:no using:yes";
       vernac_set_used_variables l
   | VernacProof (Some tac, Some l) -> 
-      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
+      Aux_file.record_in_aux_at ~loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index fb2899515f..f75f7656db 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-    Loc.t * Vernacexpr.vernac_expr -> unit
+    Vernacexpr.vernac_expr Loc.located -> unit
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name