Added an indirection with respect to Loc in Compat. As many [open Compat]

were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 93 insertions, 95 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4b7f9187fd..eca91138ed 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Pp
 open Errors
 open Util
@@ -68,7 +67,7 @@ let error_needs_inversion env x t =
 
 module type S = sig
   val compile_cases :
-    loc -> case_style ->
+    Loc.t -> case_style ->
     (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
     env -> glob_constr option * tomatch_tuples * cases_clauses ->
@@ -102,7 +101,7 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  list_make n (PatVar (dummy_loc,Anonymous))
+  list_make n (PatVar (Loc.ghost,Anonymous))
 
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -128,7 +127,7 @@ type 'a equation =
     { patterns     : cases_pattern list;
       rhs          : 'a rhs;
       alias_stack  : name list;
-      eqn_loc      : loc;
+      eqn_loc      : Loc.t;
       used         : bool ref }
 
 type 'a matrix = 'a equation list
@@ -178,7 +177,7 @@ and build_glob_pattern args = function
   | Top -> args
   | MakeConstructor (pci, rh) ->
       glob_pattern_of_partial_history
-	[PatCstr (dummy_loc, pci, args, Anonymous)] rh
+	[PatCstr (Loc.ghost, pci, args, Anonymous)] rh
 
 let complete_history = glob_pattern_of_partial_history []
 
@@ -188,12 +187,12 @@ let rec pop_history_pattern = function
   | Continuation (0, l, Top) ->
       Result (List.rev l)
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
-      feed_history (PatCstr (dummy_loc,pci,List.rev l,Anonymous)) rh
+      feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh
   | _ ->
       anomaly "Constructor not yet filled with its arguments"
 
 let pop_history h =
-  feed_history (PatVar (dummy_loc, Anonymous)) h
+  feed_history (PatVar (Loc.ghost, Anonymous)) h
 
 (* Builds a continuation expecting [n] arguments and building [ci] applied
    to this [n] arguments *)
@@ -251,7 +250,7 @@ type 'a pattern_matching_problem =
       tomatch   : tomatch_stack;
       history   : pattern_continuation;
       mat       : 'a matrix;
-      caseloc   : loc;
+      caseloc   : Loc.t;
       casestyle : case_style;
       typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
@@ -280,7 +279,7 @@ let inductive_template evdref env tmloc ind =
   let arsign = get_full_arity_sign env ind in
   let hole_source = match tmloc with
     | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
-    | None -> fun _ -> (dummy_loc, Evar_kinds.InternalHole) in
+    | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in
    let (_,evarl,_) =
     List.fold_right
       (fun (na,b,ty) (subst,evarl,n) ->
@@ -358,7 +357,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (************************************************************************)
 (* Utils *)
 
-let mkExistential env ?(src=(dummy_loc,Evar_kinds.InternalHole)) evdref =
+let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref =
   e_new_evar evdref env ~src:src (new_Type ())
 
 let evd_comb2 f evdref x y =
@@ -390,7 +389,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		let _ = e_cumul pb.env pb.evdref indt typ in
 		current
 	      else
-		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
+		(evd_comb2 (Coercion.inh_conv_coerce_to Loc.ghost pb.env)
 		  pb.evdref (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.evdref) in
 	    (current,try_find_ind pb.env sigma indt names))
@@ -914,7 +913,7 @@ let adjust_impossible_cases pb pred tomatch submat =
 	let default = (coq_unit_judge ()).uj_type in
 	pb.evdref := Evd.define evk default !(pb.evdref);
       (* we add an "assert false" case *)
-      let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in
+      let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in
       let aliasnames =
 	map_succeed (function Alias _ | NonDepAlias -> Anonymous | _ -> failwith"") tomatch
       in
@@ -924,7 +923,7 @@ let adjust_impossible_cases pb pred tomatch submat =
 		  avoid_ids = [];
 		  it = None };
 	  alias_stack = Anonymous::aliasnames;
-	  eqn_loc = dummy_loc;
+	  eqn_loc = Loc.ghost;
 	  used = ref false } ]
     | _ ->
 	submat
@@ -1207,7 +1206,7 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
   let submat = adjust_impossible_cases pb pred tomatch submat in
   if submat = [] then
     raise_pattern_matching_error
-      (dummy_loc, pb.env, NonExhaustive (complete_history history));
+      (Loc.ghost, pb.env, NonExhaustive (complete_history history));
 
   typs,
   { pb with
@@ -1531,16 +1530,16 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env t Anonymous) avoid in
-    PatVar (dummy_loc,Name id), ((id,t)::subst, id::avoid) in
+    PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match kind_of_term (whd_betadeltaiota env sigma t) with
-    | Construct cstr -> PatCstr (dummy_loc,cstr,[],Anonymous), acc
+    | Construct cstr -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
     | App (f,v) when isConstruct f ->
 	let cstr = destConstruct f in
 	let n = constructor_nrealargs env cstr in
 	let l = list_lastn n (Array.to_list v) in
 	let l,acc = list_fold_map' reveal_pattern l acc in
-	PatCstr (dummy_loc,cstr,l,Anonymous), acc
+	PatCstr (Loc.ghost,cstr,l,Anonymous), acc
     | _ -> make_patvar t acc in
   let rec aux n env acc_sign tms acc =
     match tms with
@@ -1597,7 +1596,7 @@ let build_inversion_problem loc env sigma tms t =
   let eqn1 =
     { patterns = patl;
       alias_stack = [];
-      eqn_loc = dummy_loc;
+      eqn_loc = Loc.ghost;
       used = ref false;
       rhs = { rhs_env = pb_env;
               (* we assume all vars are used; in practice we discard dependent
@@ -1610,9 +1609,9 @@ let build_inversion_problem loc env sigma tms t =
      type constraints are incompatible with the constraints on the
      inductive types of the multiple terms matched in Xi *)
   let eqn2 =
-    { patterns = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) patl;
+    { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
       alias_stack = [];
-      eqn_loc = dummy_loc;
+      eqn_loc = Loc.ghost;
       used = ref false;
       rhs = { rhs_env = pb_env;
               rhs_vars = [];
@@ -1827,7 +1826,7 @@ let mk_JMeq typ x typ' y =
   mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
 
-let hole = GHole (dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define true))
+let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true))
 
 let constr_of_pat env isevars arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
@@ -1919,13 +1918,13 @@ let vars_of_ctx ctx =
       match b with
 	| Some t' when kind_of_term t' = Rel 0 ->
 	    prev,
-	    (GApp (dummy_loc,
-		(GRef (dummy_loc, delayed_force coq_eq_refl_ref)), 
-		   [hole; GVar (dummy_loc, prev)])) :: vars
+	    (GApp (Loc.ghost,
+		(GRef (Loc.ghost, delayed_force coq_eq_refl_ref)), 
+		   [hole; GVar (Loc.ghost, prev)])) :: vars
 	| _ ->
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
-	      | Name n -> n, GVar (dummy_loc, n) :: vars)
+	      | Name n -> n, GVar (Loc.ghost, n) :: vars)
       ctx (id_of_string "vars_of_ctx_error", [])
   in List.rev y
 
@@ -2060,13 +2059,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
-	   let bref = GVar (dummy_loc, branch_name) in
+	   let bref = GVar (Loc.ghost, branch_name) in
 	     match vars_of_ctx rhs_rels with
 		 [] -> bref
-	       | l -> GApp (dummy_loc, bref, l)
+	       | l -> GApp (Loc.ghost, bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> GApp (dummy_loc, branch, [ hole ])
+	     Some _ -> GApp (Loc.ghost, branch, [ hole ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7add91c161..6e2b823dbc 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -31,24 +31,24 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * pattern_matching_error
 
-val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a
+val raise_pattern_matching_error : (Loc.t * env * pattern_matching_error) -> 'a
 
-val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a
 
-val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
 
-val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a
+val error_bad_constructor_loc : Loc.t -> constructor -> inductive -> 'a
 
-val error_bad_pattern_loc : loc -> constructor -> constr -> 'a
+val error_bad_pattern_loc : Loc.t -> constructor -> constr -> 'a
 
-val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a
+val error_wrong_predicate_arity_loc : Loc.t -> env -> constr -> constr -> constr -> 'a
 
 val error_needs_inversion : env -> constr -> types -> 'a
 
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
-  loc -> case_style ->
+  Loc.t -> case_style ->
   (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
   type_constraint ->
   env -> glob_constr option * tomatch_tuples * cases_clauses ->
@@ -75,7 +75,7 @@ type 'a equation =
     { patterns     : cases_pattern list;
       rhs          : 'a rhs;
       alias_stack  : name list;
-      eqn_loc      : loc;
+      eqn_loc      : Loc.t;
       used         : bool ref }
 
 type 'a matrix = 'a equation list
@@ -110,7 +110,7 @@ type 'a pattern_matching_problem =
       tomatch   : tomatch_stack;
       history   : pattern_continuation;
       mat       : 'a matrix;
-      caseloc   : loc;
+      caseloc   : Loc.t;
       casestyle : case_style;
       typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index b2e41841ee..1896517357 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -26,36 +26,36 @@ val inh_app_fun :
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type a sort; it fails if no coercion is applicable *)
-val inh_coerce_to_sort : loc ->
+val inh_coerce_to_sort : Loc.t ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
 
 (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type its base type (the notion depends on the coercion system) *)
-val inh_coerce_to_base : loc ->
+val inh_coerce_to_base : Loc.t ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
-val inh_coerce_to_prod : loc ->
+val inh_coerce_to_prod : Loc.t ->
   env -> evar_map -> types -> evar_map * types
 
-(** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
+(** [inh_conv_coerce_to Loc.t env isevars j t] coerces [j] to an object of type
     [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
     [j.uj_type] are convertible; it fails if no coercion is applicable *)
-val inh_conv_coerce_to : loc ->
+val inh_conv_coerce_to : Loc.t ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
-val inh_conv_coerce_rigid_to : loc ->
+val inh_conv_coerce_rigid_to : Loc.t ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
     is coercible to an object of type [t'] adding evar constraints if needed;
     it fails if no coercion exists *)
-val inh_conv_coerces_to : loc ->
+val inh_conv_coerces_to : Loc.t ->
   env -> evar_map -> types -> types -> evar_map
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
     raises [Not_found] if no coercion found *)
 val inh_pattern_coerce_to :
-  loc  -> cases_pattern -> inductive -> inductive -> cases_pattern
+  Loc.t  -> cases_pattern -> inductive -> inductive -> cases_pattern
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b6d460a85d..7ed29ba39e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -30,7 +30,7 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 
-let dl = dummy_loc
+let dl = Loc.ghost
 
 (** Should we keep details of universes during detyping ? *)
 let print_universes = ref false
@@ -687,12 +687,12 @@ let rec subst_glob_constr subst raw =
 let simple_cases_matrix_of_branches ind brs =
   List.map (fun (i,n,b) ->
       let nal,c = it_destRLambda_or_LetIn_names n b in
-      let mkPatVar na = PatVar (dummy_loc,na) in
-      let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in
+      let mkPatVar na = PatVar (Loc.ghost,na) in
+      let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in
       let ids = map_succeed Nameops.out_name nal in
-      (dummy_loc,ids,[p],c))
+      (Loc.ghost,ids,[p],c))
     brs
 
 let return_type_of_predicate ind nrealargs_ctxt pred =
   let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in
-  (List.hd nal, Some (dummy_loc, ind, List.tl nal)), Some p
+  (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 10f23b1b2c..1c6127361a 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -34,7 +34,7 @@ val detype : bool -> identifier list -> names_context -> constr -> glob_constr
 val detype_case :
   bool -> ('a -> glob_constr) ->
   (constructor array -> int array -> 'a array ->
-    (loc * identifier list * cases_pattern list * glob_constr) list) ->
+    (Loc.t * identifier list * cases_pattern list * glob_constr) list) ->
   ('a -> int -> bool) ->
   identifier list -> inductive * case_style * int array * int ->
     'a option -> 'a -> 'a array -> glob_constr
@@ -48,7 +48,7 @@ val detype_rel_context : constr option -> identifier list -> names_context ->
 val lookup_name_as_displayed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
 
-val set_detype_anonymous : (loc -> int -> glob_constr) -> unit
+val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 127e52e9a7..a011407959 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -540,7 +540,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
     List.fold_left
       (fun (i,ks,m) b ->
 	 if m=n then (i,t2::ks, m-1) else
-	 let dloc = (dummy_loc,Evar_kinds.InternalHole) in
+	 let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
 	 (i', ev :: ks, m - 1))
       (evd,[],List.length bs - 1) bs
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index bd47badfe3..b8f216ad42 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -308,7 +308,7 @@ let push_rel_context_to_named_context env typ =
  * Entry points to define new evars   *
  *------------------------------------*)
 
-let default_source = (dummy_loc,Evar_kinds.InternalHole)
+let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
   let newevk = new_untyped_evar() in
@@ -338,7 +338,7 @@ let new_type_evar ?src ?filter evd env =
   new_evar evd' env ?src ?filter (mkSort s)
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates ty =
+let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
   let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
   evdref := evd';
   ev
@@ -1962,7 +1962,7 @@ let define_pure_evar_as_lambda env evd evk =
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
-  | _ -> error_not_product_loc dummy_loc env evd typ in
+  | _ -> error_not_product_loc Loc.ghost env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
   let id =
     next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index ea0f063fe4..77985c8d73 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -29,18 +29,18 @@ val new_untyped_evar : unit -> existential_key
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
+  evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> evar_map * constr
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
+  evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+  ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -49,7 +49,7 @@ val new_type_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
@@ -158,7 +158,7 @@ val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
 val split_tycon :
-  loc -> env ->  evar_map -> type_constraint ->
+  Loc.t -> env ->  evar_map -> type_constraint ->
     evar_map * (name * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0197af56cb..9f47987f46 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -37,7 +37,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : bool list;
-  evar_source : Evar_kinds.t located;
+  evar_source : Evar_kinds.t Loc.located;
   evar_candidates : constr list option; (* if not None, list of allowed instances *)
   evar_extra : Store.t }
 
@@ -46,7 +46,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
-  evar_source = (dummy_loc,Evar_kinds.InternalHole);
+  evar_source = (Loc.ghost,Evar_kinds.InternalHole);
   evar_candidates = None;
   evar_extra = Store.empty
 }
@@ -420,7 +420,7 @@ let define evk body evd =
 	| [] ->  evd.last_mods
         | _ -> ExistentialSet.add evk evd.last_mods }
 
-let evar_declare hyps evk ty ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates evd =
+let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates evd =
   let filter =
     if filter = None then
       List.map (fun _ -> true) (named_context_of_val hyps)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 70a18b54af..f177888715 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term
@@ -177,7 +178,7 @@ val defined_evars : evar_map -> evar_map
     It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val evar_declare :
-  named_context_val -> evar -> types -> ?src:loc * Evar_kinds.t ->
+  named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
       ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 6a26fe1d43..4caf4d531e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -19,12 +19,12 @@ open Glob_term
 
 (** Operations on [glob_constr] *)
 
-val cases_pattern_loc : cases_pattern -> loc
+val cases_pattern_loc : cases_pattern -> Loc.t
 
 val cases_predicate_names : tomatch_tuples -> name list
 
 (** Apply one argument to a glob_constr *)
-val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
+val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr
 
 val map_glob_constr :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
@@ -37,7 +37,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : identifier -> glob_constr -> bool
 val free_glob_vars : glob_constr -> identifier list
-val loc_of_glob_constr : glob_constr -> loc
+val loc_of_glob_constr : glob_constr -> Loc.t
 
 (** Conversion from glob_constr to cases pattern, if possible
 
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 123d307de9..45a14a3d41 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -15,7 +15,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
 
 (** Printing of [intro_pattern] *)
 
-val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds
+val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
 
 (** Printing of [move_location] *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index e0cc2dec37..f34b8af3da 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Errors
 open Util
 open Names
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 2410fb7ca2..23b9c4d10a 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -58,33 +58,33 @@ val jv_nf_betaiotaevar :
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env -> Evd.evar_map -> int * constr * constr ->
+  Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       constr -> constructor -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
@@ -93,10 +93,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
-  env -> Evd.evar_map -> existential_key -> constr -> loc * Evar_kinds.t -> 'b
+  env -> Evd.evar_map -> existential_key -> constr -> Loc.t * Evar_kinds.t -> 'b
 
 val error_unsolvable_implicit :
-  loc -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
+  Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
@@ -115,16 +115,16 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env -> Evd.evar_map -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
-  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env -> Evd.evar_map -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
-val error_var_not_found_loc : loc -> identifier -> 'b
+val error_var_not_found_loc : Loc.t -> identifier -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bcd2a1ad15..a494e2f932 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -21,7 +21,6 @@
 (* Secondary maintenance: collective *)
 
 
-open Compat
 open Pp
 open Errors
 open Util
@@ -74,7 +73,7 @@ let search_guard loc env possible_indexes fixdefs =
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
     (try check_fix env fix with
-       | e -> if loc = dummy_loc then raise e else Loc.raise loc e);
+       | e -> if loc = Loc.ghost then raise e else Loc.raise loc e);
     indexes
   else
     (* we now search recursively amoungst all combinations *)
@@ -87,7 +86,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    with TypeError _ -> ())
 	 (list_combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
-       if loc = dummy_loc then error errmsg else
+       if loc = Loc.ghost then error errmsg else
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
 
@@ -428,7 +427,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	      | _ ->
 		  let hj = pretype empty_tycon env evdref lvar c in
 		    error_cant_apply_not_functional_loc
-		      (join_loc floc argloc) env !evdref
+		      (Loc.merge floc argloc) env !evdref
 	      	      resj [hj]
       in
       let resj = apply_rec env 1 fj candargs args in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 9401edc2d0..776e6e94e0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -24,7 +24,7 @@ open Misctypes
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
-  Pp.loc -> env -> int list list -> rec_declaration -> int array
+  Loc.t -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types option | IsType
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index fee55e72a9..5d1e4264a4 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -16,7 +16,6 @@ open Environ
 open Nametab
 open Mod_subst
 open Constrexpr
-open Compat
 open Pp
 open Util
 open Globnames
@@ -26,8 +25,8 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of global_reference * identifier located (* Class name, method *)
-    | NoInstance of identifier located * constr list
+    | UnboundMethod of global_reference * identifier Loc.located (* Class name, method *)
+    | NoInstance of identifier Loc.located * constr list
     | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index a05258de75..f14bfef220 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Names
 open Decl_kinds
 open Term
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4bf0928dce..27e5864b35 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -123,7 +123,7 @@ let pose_all_metas_as_evars env evd t =
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
-        let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in
+        let ev = Evarutil.e_new_evar evdref env ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)
   | _ ->
@@ -782,7 +782,7 @@ let applyHead env evd n c  =
       match kind_of_term (whd_betadeltaiota env evd cty) with
       | Prod (_,c1,c2) ->
         let (evd',evar) =
-	  Evarutil.new_evar evd env ~src:(dummy_loc,Evar_kinds.GoalEvar) c1 in
+	  Evarutil.new_evar evd env ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> error "Apply_Head_Then"
   in
@@ -797,7 +797,7 @@ let is_mimick_head ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+  let (evd',j') = inh_conv_coerce_rigid_to Loc.ghost env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
   let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)