[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

5 files changed, 12 insertions, 12 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 1624dc93e..ac64ab834 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -366,7 +366,7 @@ let push_rel_context_to_named_context env sigma typ =
  * Entry points to define new evars   *
  *------------------------------------*)
 
-let default_source = (Loc.ghost,Evar_kinds.InternalHole)
+let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
 let restrict_evar evd evk filter candidates =
   let evd = Sigma.to_evar_map evd in
diff --git a/engine/evd.ml b/engine/evd.ml
index 5419a10a8..9e81ccd36 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -151,7 +151,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
-  evar_source = (Loc.ghost,Evar_kinds.InternalHole);
+  evar_source = Loc.tag @@ Evar_kinds.InternalHole;
   evar_candidates = None;
   evar_extra = Store.empty
 }
@@ -704,11 +704,11 @@ let extract_all_conv_pbs evd =
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
   match kind_of_term (fst (decompose_app t1)) with
-  | Evar (evk1,_) -> fst (evar_source evk1 evd)
+  | Evar (evk1,_) -> Some (fst (evar_source evk1 evd))
   | _ ->
   match kind_of_term (fst (decompose_app t2)) with
-  | Evar (evk2,_) -> fst (evar_source evk2 evd)
-  | _ -> Loc.ghost
+  | Evar (evk2,_) -> Some (fst (evar_source evk2 evd))
+  | _             -> None
 
 (** The following functions return the set of evars immediately
     contained in the object *)
@@ -1086,8 +1086,8 @@ let retract_coercible_metas evd =
 
 let evar_source_of_meta mv evd =
   match meta_name evd mv with
-  | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
-  | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
+  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
 
 let dependent_evar_ident ev evd =
   let evi = find evd ev in
diff --git a/engine/evd.mli b/engine/evd.mli
index 9c40c8b71..005332470 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -414,7 +414,7 @@ val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 
 (** The following functions return the set of evars immediately
     contained in the object; need the term to be evar-normal otherwise
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f054038e9..84bcecc44 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -66,7 +66,7 @@ let dependent_init =
      for type classes. *)
   let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
   (* Goals don't have a source location. *)
-  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+  let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
diff --git a/engine/uState.ml b/engine/uState.ml
index c66af02bb..c9653b6cd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -266,10 +266,10 @@ let universe_context ?names ctx =
            try
              let info =
                Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
-             Option.default Loc.ghost info.uloc
-           with Not_found -> Loc.ghost
+             info.uloc
+           with Not_found -> None
          in
-           user_err ~loc ~hdr:"universe_context"
+           user_err ?loc ~hdr:"universe_context"
                         ((str(CString.plural n "Universe") ++ spc () ++
 			     Univ.LSet.pr (pr_uctx_level ctx) left ++
 			   spc () ++ str (CString.conjugate_verb_to_be n) ++