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

22 files changed, 154 insertions, 147 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 27cebf9e6..282b2c733 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -74,43 +74,43 @@ let raw_cases_pattern_expr_loc = function
 
 let local_binder_loc = function
   | LocalRawAssum ((loc,_)::_,_,t)
-  | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
+  | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
   | LocalRawAssum ([],_,_) -> assert false
 
 let local_binders_loc bll =
-  if bll = [] then dummy_loc else
-  join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+  if bll = [] then Loc.ghost else
+  Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
 
 (** Pseudo-constructors *)
 
-let mkIdentC id  = CRef (Ident (dummy_loc, id))
+let mkIdentC id  = CRef (Ident (Loc.ghost, id))
 let mkRefC r     = CRef r
-let mkCastC (a,k)  = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
-let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
+let mkCastC (a,k)  = CCast (Loc.ghost,a,k)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
+let mkLetInC (id,a,b)   = CLetIn (Loc.ghost,id,a,b)
+let mkProdC (idl,bk,a,b)   = CProdN (Loc.ghost,[idl,bk,a],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
   match f with
-  | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
-  | _ -> CApp (dummy_loc, (None, f), l)
+  | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
+  | _ -> CApp (Loc.ghost, (None, f), l)
 
 let rec mkCProdN loc bll c =
   match bll with
   | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
+      CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c)
   | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+      CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c)
   | [] -> c
   | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
 
 let rec mkCLambdaN loc bll c =
   match bll with
   | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
+      CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c)
   | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+      CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c)
   | [] -> c
   | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
 
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d3e32da46..a90a31950 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Libnames
@@ -16,12 +17,12 @@ open Constrexpr
 
 (** Constrexpr_ops: utilities on [constr_expr] *)
 
-val constr_loc : constr_expr -> loc
+val constr_loc : constr_expr -> Loc.t
 
-val cases_pattern_expr_loc : cases_pattern_expr -> loc
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> loc
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
+val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
 
-val local_binders_loc : local_binder list -> loc
+val local_binders_loc : local_binder list -> Loc.t
 
 val default_binder_kind : binder_kind
 
@@ -41,8 +42,8 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 (** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
-val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
-val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
+val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
 
 (** For binders parsing *)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c90bbf4f8..86308b6a0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -130,7 +130,7 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
 
 let insert_delimiters e = function
   | None -> e
-  | Some sc -> CDelimiters (dummy_loc,sc,e)
+  | Some sc -> CDelimiters (Loc.ghost,sc,e)
 
 let insert_pat_delimiters loc p = function
   | None -> p
@@ -220,7 +220,7 @@ let rec check_same_type ty1 ty2 =
   | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
+        List.iter2 (Loc.located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
         check_same_type r1 r2) brl1 brl2
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -260,7 +260,7 @@ let same c d = try check_same_type c d; true with _ -> false
 (* mapping patterns to cases_pattern_expr                                *)
 
 let add_patt_for_params ind l =
-    Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (dummy_loc,None)) l
+    Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -485,7 +485,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      apply_notation_to_pattern dummy_loc (IndRef ind)
+      apply_notation_to_pattern Loc.ghost (IndRef ind)
 	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
 	No_match -> extern_symbol_ind_pattern allscopes vars ind args rules
@@ -494,9 +494,9 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   if !in_debugger||Inductiveops.inductive_has_local_defs ind then
-    let c = extern_reference dummy_loc vars (IndRef ind) in
+    let c = extern_reference Loc.ghost vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-    CPatCstr (dummy_loc, c, add_patt_for_params ind args, [])
+    CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
   else
     try
       if !Flags.raw_print or !print_no_symbol then raise No_match;
@@ -504,18 +504,18 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
 	| Some key ->
-	  insert_pat_delimiters dummy_loc (CPatPrim(dummy_loc,p)) key
+	  insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key
     with No_match ->
       try
 	if !Flags.raw_print or !print_no_symbol then raise No_match;
 	extern_symbol_ind_pattern scopes vars ind args
 	  (uninterp_ind_pattern_notations ind)
     with No_match ->
-      let c = extern_reference dummy_loc vars (IndRef ind) in
+      let c = extern_reference Loc.ghost vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
-	   |Some true_args -> CPatCstr (dummy_loc, c, [], true_args)
-	   |None -> CPatCstr (dummy_loc, c, args, [])
+	   |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args)
+	   |None -> CPatCstr (Loc.ghost, c, args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
@@ -561,7 +561,7 @@ let explicitize loc inctx impl (cf,f) args =
 	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then
-	  (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
+	  (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
 	else
 	  tail
     | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
@@ -756,12 +756,12 @@ let rec extern inctx scopes vars r =
   | GProd (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
-      CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
+      CProdN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
 
   | GLambda (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
-      CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
+      CLambdaN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
 
   | GCases (loc,sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -772,13 +772,13 @@ let rec extern inctx scopes vars r =
       let na' = match na,tm with
           Anonymous, GVar (_,id) when
 	      rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
-	      -> Some (dummy_loc,Anonymous)
+	      -> Some (Loc.ghost,Anonymous)
         | Anonymous, _ -> None
         | Name id, GVar (_,id') when id=id' -> None
-        | Name _, _ -> Some (dummy_loc,na) in
+        | Name _, _ -> Some (Loc.ghost,na) in
       (sub_extern false scopes vars tm,
        (na',Option.map (fun (loc,ind,nal) ->
-	 let args = List.map (fun x -> PatVar (dummy_loc, x)) nal in
+	 let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
 	 let fullargs = Notation_ops.add_patterns_for_params ind args in
 	 extern_ind_pattern_in_scope scopes vars ind fullargs
 	) x))) tml in
@@ -786,15 +786,15 @@ let rec extern inctx scopes vars r =
     CCases (loc,sty,rtntypopt',tml,eqns)
 
   | GLetTuple (loc,nal,(na,typopt),tm,b) ->
-      CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
-        (Option.map (fun _ -> (dummy_loc,na)) typopt,
+      CLetTuple (loc,List.map (fun na -> (Loc.ghost,na)) nal,
+        (Option.map (fun _ -> (Loc.ghost,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | GIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (Option.map (fun _ -> (dummy_loc,na)) typopt,
+        (Option.map (fun _ -> (Loc.ghost,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
@@ -811,10 +811,10 @@ let rec extern inctx scopes vars r =
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (dummy_loc, out_name (List.nth assums x))
+		     | Some x -> Some (Loc.ghost, out_name (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
-		 ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
+		 ((Loc.ghost, fi), (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
@@ -824,7 +824,7 @@ let rec extern inctx scopes vars r =
                  let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
-		 ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i),
+		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
@@ -873,7 +873,7 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Idset.add na vars) l in
       (assums,na::ids,
-       LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
+       LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
   | (na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
@@ -883,10 +883,10 @@ and extern_local_binder scopes vars = function
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
-               LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
+               LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l)
         | (assums,ids,l) ->
             (na::assums,na::ids,
-             LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
+             LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
@@ -915,7 +915,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                   subscopes,impls
                 | _ ->
                   [], [] in
-	      (if n = 0 then f else GApp (dummy_loc,f,args1)),
+	      (if n = 0 then f else GApp (Loc.ghost,f,args1)),
 	      args2, subscopes, impls
 	  | GApp (_,(GRef (_,ref) as f),args), None ->
 	      let subscopes = find_arguments_scope ref in
@@ -923,7 +923,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 		  select_impargs_size
 		    (List.length args) (implicits_of_global ref) in
 	      f, args, subscopes, impls
-	  | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], []
+	  | GRef _, Some 0 -> GApp (Loc.ghost,t,[]), [], [], []
           | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
@@ -983,7 +983,7 @@ let extern_glob_type vars c =
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
 
-let loc = dummy_loc (* for constr and pattern, locations are lost *)
+let loc = Loc.ghost (* for constr and pattern, locations are lost *)
 
 let extern_constr_gen goal_concl_style scopt env t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0c5d4b589..9f7acbc6d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -37,7 +37,7 @@ val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
 
 val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
-val extern_reference : loc -> Idset.t -> global_reference -> reference
+val extern_reference : Loc.t -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
 val extern_sort : sorts -> glob_sort
 val extern_rel_context : constr option -> env ->
@@ -55,7 +55,7 @@ val print_projections : bool ref
 
 (** Debug printing options *)
 val set_debug_global_reference_printer :
-  (loc -> global_reference -> reference) -> unit
+  (Loc.t -> global_reference -> reference) -> unit
 val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f6513fd0d..880afe57d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -119,7 +119,7 @@ type internalization_error =
   | BadPatternsNumber of int * int
   | BadExplicitationNumber of explicitation * int option
 
-exception InternalizationError of loc * internalization_error
+exception InternalizationError of Loc.t * internalization_error
 
 let explain_variable_capture id id' =
   pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
@@ -325,12 +325,12 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 
 let rec it_mkGProd loc2 env body =
   match env with
-      (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (join_loc loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
     | [] -> body
 
 let rec it_mkGLambda loc2 env body =
   match env with
-      (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (join_loc loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -474,10 +474,10 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -738,7 +738,7 @@ let intern_applied_reference intern env namedctx lvar args = function
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
-    intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
+    intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
       {ids = Idset.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
       (vars,[]) [] r
@@ -800,7 +800,7 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs =
- join_loc (fst (List.hd lhs)) (fst (list_last lhs))
+ Loc.merge (fst (List.hd lhs)) (fst (list_last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -840,10 +840,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else args_len = nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,RCPatAtom(dummy_loc,None)::out)
+      then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,RCPatAtom(dummy_loc,None)::out)
+      then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -883,7 +883,7 @@ let find_constructor loc add_params ref =
     |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
       then fst (Inductiveops.inductive_nargs ind)
       else Inductiveops.inductive_nparams ind in
-		     Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))])
+		     Util.list_make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
     |None -> []) cstr
 
 let find_pattern_variable = function
@@ -1312,7 +1312,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
 					       push_name_env lvar (impls_type_list ~args:fix_args tyi)
-					    en (dummy_loc, Name name)) 0 env' lf in
+					    en (Loc.ghost, Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	GRec (loc,GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
@@ -1339,7 +1339,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
 	       push_name_env lvar (impls_type_list ~args:cofix_args tyi)
-					    en (dummy_loc, Name name)) 0 env' lf in
+					    en (Loc.ghost, Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	GRec (loc,GCoFix n,
               Array.of_list lf,
@@ -1396,7 +1396,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
-	  | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args)
+	  | GApp (loc', f', args') -> GApp (Loc.merge loc' loc, f',args'@args)
 	  | _ -> GApp (loc, c, args))
     | CRecord (loc, _, fs) ->
 	let cargs =
@@ -1424,7 +1424,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  (tm,ind)::inds, Option.fold_right Idset.add extra_id ex_ids, List.rev_append match_td matchs)
 	    tms ([],Idset.empty,[]) in
       let env' = Idset.fold
-	(fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (dummy_loc,Name var))
+	(fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var))
 	(Idset.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
       (* PatVars before a real pattern do not need to be matched *)
       let stripped_match_from_in = let rec aux = function
@@ -1436,12 +1436,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
 	  | l -> let thevars,thepats=List.split l in
 		 Some (
-		   GCases(dummy_loc,Term.RegularStyle,Some (GSort (dummy_loc,GType None)), (* "return Type" *)
-			  List.map (fun id -> GVar (dummy_loc,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
-			  [dummy_loc,[],thepats, (* "|p1,..,pn" *)
-			   Option.cata (intern_type env') (GHole(dummy_loc,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
-			   dummy_loc,[],list_make (List.length thepats) (PatVar(dummy_loc,Anonymous)), (* "|_,..,_" *)
-			   GHole(dummy_loc,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
+		   GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *)
+			  List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
+			  [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
+			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
+			   Loc.ghost,[],list_make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
@@ -1451,7 +1451,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let ((b',(na',_)),_,_) = intern_case_item env' Idset.empty (b,(na,None)) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
-	    (dummy_loc,na') in
+	    (Loc.ghost,na') in
 	  intern_type env'' u) po in
         GLetTuple (loc, List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
@@ -1460,7 +1460,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
       let ((c',(na',_)),_,_) = intern_case_item env' Idset.empty (c,(na,None)) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
-	    (dummy_loc,na') in
+	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) ->
@@ -1516,7 +1516,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let extra_id,na = match tm', na with
       | GVar (loc,id), None when Idset.mem id env.ids -> Some id,(loc,Name id)
       | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
-      | _, None -> None,(dummy_loc,Anonymous)
+      | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
     let match_td,typ = match t with
@@ -1540,7 +1540,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      |(_,Some _,_)::t, l when not with_letin ->
-		canonize_args t l forbidden_names match_acc ((dummy_loc,Anonymous)::var_acc)
+		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
 	      |[],[] ->
 		(add_name match_acc na, var_acc)
 	      |_::t,PatVar (loc,x)::tt ->
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 6f01bb466..39c307bcb 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -76,7 +76,7 @@ let check_required_library d =
 (* Loading silently ...
     let m, prefix = list_sep_last d' in
     read_library
-     (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
+     (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
 (* or failing ...*)
       error ("Library "^(string_of_dirpath dir)^" has to be required first.")
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 9fde5e219..e56d3b9ae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -119,7 +119,7 @@ let remove_sections dir =
     dir
 
 let interval loc =
-  let loc1,loc2 = Pp.unloc loc in
+  let loc1,loc2 = Loc.unloc loc in
   loc1, loc2-1
 
 let dump_ref loc filepath modpath ident ty =
@@ -138,7 +138,7 @@ let add_glob_gen loc sp lib_dp ty =
       dump_ref loc filepath modpath ident ty
 
 let add_glob loc ref =
-  if dump () && loc <> Pp.dummy_loc then
+  if dump () && loc <> Loc.ghost then
     let sp = Nametab.path_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
@@ -149,7 +149,7 @@ let mp_of_kn kn =
     Names.MPdot (mp,l)
 
 let add_glob_kn loc kn =
-  if dump () && loc <> Pp.dummy_loc then
+  if dump () && loc <> Loc.ghost then
     let sp = Nametab.path_of_syndef kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
@@ -232,7 +232,7 @@ let cook_notation df sc =
 
 let dump_notation (loc,(df,_)) sc sec =
   (* We dump the location of the opening '"' *)
-  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Pp.unloc loc))
+  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Loc.unloc loc))
     (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 469df1222..73354fa40 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -22,19 +22,19 @@ val dump_to_dotglob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val add_glob : Pp.loc -> Globnames.global_reference -> unit
-val add_glob_kn : Pp.loc -> Names.kernel_name -> unit
-
-val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit
-val dump_moddef : Pp.loc -> Names.module_path -> string -> unit
-val dump_modref  : Pp.loc -> Names.module_path -> string -> unit
-val dump_reference  : Pp.loc -> string -> string -> string -> unit
-val dump_libref : Pp.loc -> Names.dir_path -> string -> unit
+val add_glob : Loc.t -> Globnames.global_reference -> unit
+val add_glob_kn : Loc.t -> Names.kernel_name -> unit
+
+val dump_definition : Loc.t * Names.identifier -> bool -> string -> unit
+val dump_moddef : Loc.t -> Names.module_path -> string -> unit
+val dump_modref  : Loc.t -> Names.module_path -> string -> unit
+val dump_reference  : Loc.t -> string -> string -> string -> unit
+val dump_libref : Loc.t -> Names.dir_path -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
-val dump_binding : Pp.loc -> Names.Idset.elt -> unit
+val dump_binding : Loc.t -> Names.Idset.elt -> unit
 val dump_notation :
-  Pp.loc * (Constrexpr.notation * Notation.notation_location) ->
+  Loc.t * (Constrexpr.notation * Notation.notation_location) ->
   Notation_term.scope_name option -> bool -> unit
 val dump_constraint :
   Constrexpr.typeclass_constraint -> bool -> string -> unit
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 2bd19632e..51266b5eb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term
@@ -19,7 +20,7 @@ open Term
 open Evd
 open Misctypes
 
-val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
    in the environment by the effective calls to Intro, Inversion, etc 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 9389a1690..69f70deef 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -60,7 +60,7 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
 
-let in_generalizable : bool * identifier located list option -> obj =
+let in_generalizable : bool * identifier Loc.located list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
@@ -253,7 +253,7 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, (na, _, _)) ->
     let id' = next_name_away_from na avoid in
-      (CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
+      (CRef (Ident (Loc.ghost, id')), Idset.add id' avoid)
 
 let destClassApp cl =
   match cl with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 6297a17d2..5aa77f708 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Names
 open Decl_kinds
 open Term
@@ -24,8 +25,8 @@ open Typeclasses
 val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
 
 val ids_of_list : identifier list -> Idset.t
-val destClassApp : constr_expr -> loc * reference * constr_expr list
-val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
@@ -39,7 +40,7 @@ val free_vars_of_binders :
    order with the location of their first occurence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
-  glob_constr -> (Names.identifier * loc) list
+  glob_constr -> (Names.identifier * Loc.t) list
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 18d3a9c1c..d3468c463 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -46,19 +46,19 @@ let error_result_must_be_signature () =
   error "The result module type must be a signature."
 
 let error_not_a_modtype_loc loc s =
-  Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
+  Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
 
 let error_not_a_module_loc loc s =
-  Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s))
+  Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s))
 
 let error_not_a_module_nor_modtype_loc loc s =
-  Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
+  Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
 
 let error_incorrect_with_in_module loc =
-  Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
+  Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
 
 let error_application_to_module_type loc =
-  Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
+  Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
 
 
 
@@ -149,7 +149,7 @@ let loc_of_module = function
 let check_module_argument_is_path me' = function
   | CMident _ -> ()
   | (CMapply (loc,_,_) | CMwith (loc,_,_)) ->
-      Compat.Loc.raise loc
+      Loc.raise loc
         (Modops.ModuleTypingError (Modops.ApplicationToNotPath me'))
 
 let rec interp_modexpr env = function
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 860f66790..fc3617ce2 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Declarations
 open Environ
 open Entries
diff --git a/interp/notation.ml b/interp/notation.ml
index a76ede48c..e42bd787c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -219,7 +219,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 -> 'a -> glob_constr
+    Loc.t -> 'a -> glob_constr
 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
@@ -227,7 +227,7 @@ type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
-    loc -> prim_token -> required_module * (unit -> glob_constr)
+    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)
@@ -416,8 +416,8 @@ let uninterp_prim_token_ind_pattern ind args =
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = GRef (dummy_loc,ref) in
-    match numpr (GApp (dummy_loc,ref,args')) with
+    let ref = GRef (Loc.ghost,ref) in
+    match numpr (GApp (Loc.ghost,ref,args')) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
@@ -435,7 +435,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 dummy_loc n); true
+    try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost 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)
@@ -654,7 +654,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 dummy_loc c)
+  prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
 
 let pr_named_scope prglob scope sc =
  (if scope = default_scope then
@@ -727,7 +727,7 @@ let error_notation_not_reference loc ntn =
 let interp_notation_as_global_reference loc test ntn sc =
   let scopes = match sc with
   | Some sc ->
-      Gmap.add sc (find_scope (find_delimiters_scope dummy_loc sc)) Gmap.empty
+      Gmap.add sc (find_scope (find_delimiters_scope Loc.ghost sc)) Gmap.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation test) ntns in
diff --git a/interp/notation.mli b/interp/notation.mli
index 3f66f993a..d1446527f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -54,7 +54,7 @@ val find_scope : scope_name -> scope
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
-val find_delimiters_scope : loc -> delimiters -> scope_name
+val find_delimiters_scope : Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
@@ -68,7 +68,7 @@ type required_module = full_path * string list
 type cases_pattern_status = bool (** true = use prim token in patterns *)
 
 type 'a prim_token_interpreter =
-    loc -> 'a -> glob_constr
+    Loc.t -> 'a -> glob_constr
 
 type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
@@ -82,9 +82,9 @@ val declare_string_interpreter : scope_name -> required_module ->
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : loc -> prim_token -> local_scopes ->
+val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
-val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
   local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
@@ -113,7 +113,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (** Return the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> local_scopes ->
+val interp_notation : Loc.t -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
 (** Return the possible notations for a given term *)
@@ -137,7 +137,7 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
 (** {6 Miscellaneous} *)
 
-val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
+val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
 (** Checks for already existing notations *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b1067fa47..857e827a9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -165,7 +165,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
 
 let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
 
-let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1)
+let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
   user_err_loc (loc_of_glob_constr t,"",
@@ -209,7 +209,7 @@ let compare_recursive_parts found f (iterator,subc) =
     | Some (x,y,Some lassoc) ->
 	let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
 	let iterator =
-	  f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator
+	  f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
 	  else iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
@@ -467,7 +467,7 @@ let abstract_return_type_context pi mklam tml rtno =
 let abstract_return_type_context_glob_constr =
   abstract_return_type_context (fun (_,_,nal) -> nal)
     (fun na c ->
-      GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c))
+      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole),c))
 
 let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
@@ -513,8 +513,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (_,Name id2) when List.mem id2 (fst metas) ->
       let rhs = match na1 with
-      | Name id1 -> GVar (dummy_loc,id1)
-      | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in
+      | Name id1 -> GVar (Loc.ghost,id1)
+      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in
       alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
@@ -689,8 +689,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | b1, NLambda (Name id,NHole _,b2) when inner ->
       let id' = Namegen.next_ident_away id (free_glob_vars b1) in
       match_in u alp metas (bind_binder sigma id
-       [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))])
-       (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2
+       [(Name id',Explicit,None,GHole(Loc.ghost,Evar_kinds.BinderType (Name id')))])
+       (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
 
   | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
@@ -721,7 +721,7 @@ let match_notation_constr u c (metas,pat) =
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
-      GVar (dummy_loc,x) in
+      GVar (Loc.ghost,x) in
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
     match typ with
     | NtnTypeConstr ->
@@ -736,7 +736,7 @@ let match_notation_constr u c (metas,pat) =
 let add_patterns_for_params ind l =
   let mib,_ = Global.lookup_inductive ind in
   let nparams = mib.Declarations.mind_nparams in
-    Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l
+    Util.list_addn nparams (PatVar (Loc.ghost,Anonymous)) l
 
 let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index dee1203b3..ef92500f1 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -28,12 +28,12 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
-val glob_constr_of_notation_constr_with_binders : Pp.loc ->
+val glob_constr_of_notation_constr_with_binders : Loc.t ->
   ('a -> name -> 'a * name) ->
   ('a -> notation_constr -> glob_constr) ->
   'a -> notation_constr -> glob_constr
 
-val glob_constr_of_notation_constr : Pp.loc -> notation_constr -> glob_constr
+val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
 (** [match_notation_constr] matches a [glob_constr] against a notation
     interpretation; raise [No_match] if the matching fails   *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index f170ff023..a72b10ad6 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -95,7 +95,7 @@ let anonymize_if_reserved na t = match na with
 	   (try Notation_ops.notation_constr_of_glob_constr [] [] t
 		  = find_reserved_type id
             with UserError _ -> false)
-	then GHole (dummy_loc,Evar_kinds.BinderType na)
+	then GHole (Loc.ghost,Evar_kinds.BinderType na)
 	else t
       with Not_found -> t)
   | Anonymous -> t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index d52460b08..d23bb8789 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Glob_term
 open Notation_term
 
 val declare_reserved_type : identifier located list -> notation_constr -> unit
-val find_reserved_type : identifier ->notation_constr
+val find_reserved_type : identifier -> notation_constr
 val anonymize_if_reserved : name -> glob_constr -> glob_constr
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index eaa4863c6..be9feead3 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Libnames
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index bc9d3b851..8ec834d76 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -59,7 +59,7 @@ let ids_of_cases_tomatch tms =
   List.fold_right
     (fun (_,(ona,indnal)) l ->
       Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (Option.fold_right (down_located name_cons) ona l))
+      indnal (Option.fold_right (Loc.down_located name_cons) ona l))
     tms []
 
 let is_constructor id =
@@ -84,7 +84,7 @@ let rec cases_pattern_fold_names f a = function
 
 let ids_of_pattern_list =
   List.fold_left
-    (located_fold_left
+    (Loc.located_fold_left
       (List.fold_left (cases_pattern_fold_names Idset.add)))
     Idset.empty
 
@@ -117,7 +117,7 @@ let fold_constr_expr_with_binders g f n acc = function
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
-      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None)) bl) acc bll
   | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
@@ -131,12 +131,12 @@ let fold_constr_expr_with_binders g f n acc = function
 	let ids = ids_of_pattern_list patl in
 	f (Idset.fold g ids n) acc rhs) bl acc
   | CLetTuple (loc,nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (name_fold g)) nal n in
-      f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+      let n' = List.fold_right (Loc.down_located (name_fold g)) nal n in
+      f (Option.fold_right (Loc.down_located (name_fold g)) ona n') (f n acc b) c
   | CIf (_,c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-	(f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+	(f (Option.fold_right (Loc.down_located (name_fold g)) ona n)) acc po
   | CFix (loc,_,l) ->
       let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -177,7 +177,7 @@ let split_at_annot bl na =
 
 (* Used in correctness and interface *)
 
-let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (Loc.down_located (name_fold g)) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -221,11 +221,11 @@ let map_constr_expr_with_binders g f e = function
       let po = Option.map (f (List.fold_right g ids e)) rtnpo in
       CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (name_fold g)) nal e in
-      let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
+      let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
       CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
   | CIf (loc,c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
       CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
@@ -254,20 +254,20 @@ let rec replace_vars_constr_expr l = function
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast =
-  | CWith_Module of identifier list located * qualid located
-  | CWith_Definition of identifier list located * constr_expr
+  | CWith_Module of identifier list Loc.located * qualid Loc.located
+  | CWith_Definition of identifier list Loc.located * constr_expr
 
 type module_ast =
-  | CMident of qualid located
-  | CMapply of loc * module_ast * module_ast
-  | CMwith of loc * module_ast * with_declaration_ast
+  | CMident of qualid Loc.located
+  | CMapply of Loc.t * module_ast * module_ast
+  | CMwith of Loc.t * module_ast * with_declaration_ast
 
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
 (* and which are then occupied by proper symbols of the notation (or spaces) *)
 
 let locs_of_notation loc locs ntn =
-  let (bl,el) = unloc loc in
-  let locs =  List.map unloc locs in
+  let (bl, el) = Loc.unloc loc in
+  let locs =  List.map Loc.unloc locs in
   let rec aux pos = function
     | [] -> if pos = el then [] else [(pos,el-1)]
     | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index bd9e776c9..d99846d12 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Libnames
@@ -47,10 +48,10 @@ val map_constr_expr_with_binders :
       'a -> constr_expr -> constr_expr
 
 val ntn_loc :
-  loc -> constr_notation_substitution -> string -> (int * int) list
+  Loc.t -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
-  loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+  Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
 
 (** For cases pattern parsing errors *)
 
-val error_invalid_pattern_notation : Pp.loc -> 'a
+val error_invalid_pattern_notation : Loc.t -> 'a