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

23 files changed, 158 insertions, 159 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 78ffda215..d0fdfa0f3 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -77,13 +77,13 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr=
 
 
 type raw_proof_instr =
-    ((identifier*(Constrexpr.constr_expr option)) located,
+    ((identifier*(Constrexpr.constr_expr option)) Loc.located,
      Constrexpr.constr_expr,
      Constrexpr.cases_pattern_expr,
      raw_tactic_expr) gen_proof_instr
 
 type glob_proof_instr =
-    ((identifier*(Genarg.glob_constr_and_expr option)) located,
+    ((identifier*(Genarg.glob_constr_and_expr option)) Loc.located,
      Genarg.glob_constr_and_expr,
      Constrexpr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a067440cb..da3f9619b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -18,7 +18,6 @@ open Pretyping
 open Glob_term
 open Term
 open Pp
-open Compat
 open Decl_kinds
 open Misctypes
 
@@ -188,16 +187,16 @@ let interp_constr_or_thesis check_sort sigma env = function
 let abstract_one_hyp inject h glob =
   match h with
       Hvar (loc,(id,None)) ->
-	GProd (dummy_loc,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob)
+	GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob)
     | Hvar (loc,(id,Some typ)) ->
-	GProd (dummy_loc,Name id, Explicit, fst typ, glob)
+	GProd (Loc.ghost,Name id, Explicit, fst typ, glob)
     | Hprop st ->
-	GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob)
+	GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob)
 
 let glob_constr_of_hyps inject hyps head =
   List.fold_right (abstract_one_hyp inject) hyps head
 
-let glob_prop = GSort (dummy_loc,GProp)
+let glob_prop = GSort (Loc.ghost,GProp)
 
 let rec match_hyps blend names constr = function
     [] -> [],substl names constr
@@ -245,27 +244,27 @@ let rec glob_of_pat =
 	let mind= fst (Global.lookup_inductive ind) in
 	let rec add_params n q =
 	  if n<=0 then q else
-	    add_params (pred n) (GHole(dummy_loc,
+	    add_params (pred n) (GHole(Loc.ghost,
 				       Evar_kinds.TomatchTypeParameter(ind,n))::q) in
 	    let args = List.map glob_of_pat lpat in
-	      glob_app(loc,GRef(dummy_loc,Globnames.ConstructRef cstr),
+	      glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr),
 		   add_params mind.Declarations.mind_nparams args)
 
 let prod_one_hyp = function
     (loc,(id,None)) ->
       (fun glob ->
-	 GProd (dummy_loc,Name id, Explicit,
+	 GProd (Loc.ghost,Name id, Explicit,
 		GHole (loc,Evar_kinds.BinderType (Name id)), glob))
   | (loc,(id,Some typ)) ->
       (fun glob ->
-	 GProd (dummy_loc,Name id, Explicit, fst typ, glob))
+	 GProd (Loc.ghost,Name id, Explicit, fst typ, glob))
 
 let prod_one_id (loc,id) glob =
-  GProd (dummy_loc,Name id, Explicit,
+  GProd (Loc.ghost,Name id, Explicit,
 	 GHole (loc,Evar_kinds.BinderType (Name id)), glob)
 
 let let_in_one_alias (id,pat) glob =
-  GLetIn (dummy_loc,Name id, glob_of_pat pat, glob)
+  GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -335,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	     (if expected = 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
-    let rind = GRef (dummy_loc,Globnames.IndRef pinfo.per_ind) in
+    let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in
     let rparams = List.map detype_ground pinfo.per_params in
     let rparams_rec =
       List.map
@@ -343,18 +342,18 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	   GVar (loc,id)) params in
     let dum_args=
       list_tabulate
-	(fun _ -> GHole (dummy_loc,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
+	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
 	oib.Declarations.mind_nrealargs in
-      glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
+      glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
-      Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp)
+      Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
     | Thesis (For rec_occ) ->
 	if not (List.mem rec_occ pat_vars) then
 	  errorlabstrm "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
-	Glob_term.GSort(dummy_loc,GProp)
+	Glob_term.GSort(Loc.ghost,GProp)
     | This (c,_) -> c in
   let term1 = glob_constr_of_hyps inject hyps glob_prop in
   let loc_ids,npatt =
@@ -362,8 +361,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
     let npatt= deanonymize rids patt in
       List.rev (fst !rids),npatt in
   let term2 =
-    GLetIn(dummy_loc,Anonymous,
-	   GCast(dummy_loc,glob_of_pat npatt,
+    GLetIn(Loc.ghost,Anonymous,
+	   GCast(Loc.ghost,glob_of_pat npatt,
 		 CastConv app_ind),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
@@ -418,11 +417,11 @@ let interp_casee sigma env = function
 let abstract_one_arg = function
     (loc,(id,None)) ->
       (fun glob ->
-	 GLambda (dummy_loc,Name id, Explicit,
+	 GLambda (Loc.ghost,Name id, Explicit,
 		GHole (loc,Evar_kinds.BinderType (Name id)), glob))
   | (loc,(id,Some typ)) ->
       (fun glob ->
-	 GLambda (dummy_loc,Name id, Explicit, fst typ, glob))
+	 GLambda (Loc.ghost,Name id, Explicit, fst typ, glob))
 
 let glob_constr_of_fun args body =
   List.fold_right abstract_one_arg args (fst body)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 2d069b497..b59ab5c0f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -751,7 +751,7 @@ let consider_tac c hyps gls =
     | _ ->
 	let id = pf_get_new_id (id_of_string "_tmp") gls in
 	tclTHEN
-	  (forward None (Some (dummy_loc, IntroIdentifier id)) c)
+	  (forward None (Some (Loc.ghost, IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls
 
 
@@ -1290,7 +1290,7 @@ let understand_my_constr c gls =
   let nc = names_of_rel_context env in
   let rawc = Detyping.detype false [] nc c in
   let rec frob = function
-    | GEvar _ -> GHole (dummy_loc,Evar_kinds.QuestionMark Evar_kinds.Expand)
+    | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand)
     | rc ->  map_glob_constr frob rc
   in
   Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b009107dc..3f0c704ad 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -107,7 +107,7 @@ open Genarg
 open Ppconstr
 open Printer
 let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference
-let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global))
+let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global))
 let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
 
 ARGUMENT EXTEND firstorder_using
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index bc15cb501..195e6afa3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -128,7 +128,7 @@ let mk_open_instance id gl m t=
       match t with
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (dummy_loc,Evar_kinds.BinderType name),t1)
+	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1)
 	| _-> anomaly "can't happen" in
   let ntt=try
     Pretyping.understand evmap env (raux m rawt)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 169f4d120..9fcfeb36c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -139,7 +139,7 @@ module FunctionGram =
 struct
   let gec s = Gram.entry_create ("Function."^s)
 		(* types *)
-  let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located Gram.entry = gec "function_rec_definition_loc"
+  let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located Gram.entry = gec "function_rec_definition_loc"
 end
 open FunctionGram
 
@@ -151,7 +151,7 @@ GEXTEND Gram
     ;
 
   END
-type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located, 'a) Genarg.abstract_argument_type
+type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type
 
 let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
   (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
@@ -460,9 +460,9 @@ VERNAC COMMAND EXTEND MergeFunind
       "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
      [
        let f1 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Pp.dummy_loc,id1))) in
+	 (CRef (Libnames.Ident (Loc.ghost,id1))) in
        let f2 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Pp.dummy_loc,id2))) in
+	 (CRef (Libnames.Ident (Loc.ghost,id2))) in
        let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
        let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
        let ar1 = List.length (fst (decompose_prod f1type)) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7b341e581..93e1d105e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -273,8 +273,8 @@ let make_discr_match_brl i =
   list_map_i
     (fun j (_,idl,patl,_) ->
        if j=i
-       then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref))
-       else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref))
+       then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
+       else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
     )
     0
 (*
@@ -511,9 +511,9 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		    | u::l -> 
 			match t with 
 			  | GLambda(loc,na,_,nat,b) -> 
-			      GLetIn(dummy_loc,na,u,aux b l)
+			      GLetIn(Loc.ghost,na,u,aux b l)
 			  | _ -> 
-			      GApp(dummy_loc,t,l)
+			      GApp(Loc.ghost,t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
 	    | GVar(_,id) when Idset.mem id funnames ->
@@ -571,7 +571,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (GVar(dummy_loc,id))
+			    (GVar(Loc.ghost,id))
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -661,7 +661,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	assert (Array.length case_pats = 2);
 	let brl =
 	  list_map_i
-	    (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
+	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
 	in
@@ -692,7 +692,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let case_pats = build_constructors_of_type ind nal_as_glob_constr in
 	  assert (Array.length case_pats = 1);
 	  let br =
-	    (dummy_loc,[],[case_pats.(0)],e)
+	    (Loc.ghost,[],[case_pats.(0)],e)
 	  in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  build_entry_lc env funnames avoid match_expr
@@ -981,8 +981,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      ((Util.list_chop nparam args'))
 		    in
 		    let rt_typ =
-		       GApp(Pp.dummy_loc,
-			    GRef (Pp.dummy_loc,Globnames.IndRef ind),
+		       GApp(Loc.ghost,
+			    GRef (Loc.ghost,Globnames.IndRef ind),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
@@ -1130,7 +1130,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		then
 		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
 		else
-		  GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  GProd(Loc.ghost,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here"
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
@@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Idset.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
-	    | _ -> GLetIn(dummy_loc,n,t,new_b),
+	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
 		Idset.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
@@ -1175,7 +1175,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 (* 	    | Name id when Idset.mem id id_to_exclude ->  *)
 (* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  GLetTuple(dummy_loc,nal,(na,None),t,new_b),
+	  GLetTuple(Loc.ghost,nal,(na,None),t,new_b),
 		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
 
 	end
@@ -1261,9 +1261,9 @@ let rec rebuild_return_type rt =
 	Constrexpr.CProdN(loc,n,rebuild_return_type t')
     | Constrexpr.CLetIn(loc,na,t,t') ->
 	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Constrexpr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],
+    | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Names.Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,rt],
-			    Constrexpr.CSort(dummy_loc,GType None))
+			    Constrexpr.CSort(Loc.ghost,GType None))
 
 
 let do_build_inductive
@@ -1303,12 +1303,12 @@ let do_build_inductive
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
 			      acc)
 	   else
 	     Constrexpr.CProdN
-	       (dummy_loc,
-		[[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	       (Loc.ghost,
+		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 		acc
 	       )
 	)
@@ -1369,12 +1369,12 @@ let do_build_inductive
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
 			    acc)
 	 else
 	   Constrexpr.CProdN
-	   (dummy_loc,
-	   [[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	   (Loc.ghost,
+	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 	    acc
 	   )
       )
@@ -1391,17 +1391,17 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
+	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Idset.empty t)
 	 else
 	 Constrexpr.LocalRawAssum
-	   ([(dummy_loc,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
+	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
       )
       rels_params
   in
   let ext_rels_constructors =
     Array.map (List.map
       (fun (id,t) ->
-	 false,((dummy_loc,id),
+	 false,((Loc.ghost,id),
 		Flags.with_option
 		  Flags.raw_print
 		  (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t)
@@ -1410,7 +1410,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    ((dummy_loc,relnames.(i)),
+    ((Loc.ghost,relnames.(i)),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8967a3ec8..f678b898b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -11,18 +11,18 @@ let idmap_is_empty m = m = Idmap.empty
 
 (*
    Some basic functions to rebuild glob_constr
-   In each of them the location is Util.dummy_loc
+   In each of them the location is Loc.ghost
 *)
-let mkGRef ref = GRef(dummy_loc,ref)
-let mkGVar id = GVar(dummy_loc,id)
-let mkGApp(rt,rtl) = GApp(dummy_loc,rt,rtl)
-let mkGLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b)
-let mkGProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b)
-let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b)
-let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl)
-let mkGSort s = GSort(dummy_loc,s)
-let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous)
-let mkGCast(b,t) = GCast(dummy_loc,b,CastConv t)
+let mkGRef ref = GRef(Loc.ghost,ref)
+let mkGVar id = GVar(Loc.ghost,id)
+let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
+let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
+let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b)
+let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b)
+let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl)
+let mkGSort s = GSort(Loc.ghost,s)
+let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous)
+let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t)
 
 (*
   Some basic functions to decompose glob_constrs
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 437ba225d..9cf83df15 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -15,7 +15,7 @@ val pattern_to_term : cases_pattern -> glob_constr
 
 (*
    Some basic functions to rebuild glob_constr
-   In each of them the location is Util.dummy_loc
+   In each of them the location is Util.Loc.ghost
 *)
 val mkGRef : Globnames.global_reference -> glob_constr
 val mkGVar : Names.identifier -> glob_constr
@@ -85,9 +85,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Names.identifier list ->
-    Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
     Glob_term.glob_constr ->
-    Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
     Glob_term.glob_constr
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2a6a7dea3..5b9bf44c3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -182,7 +182,7 @@ let build_newrecursive l =
        match body_opt with 
 	 | Some body -> 
 	     (fixna,bll,ar,body)
-	 | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given")
+	 | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given")
     ) l
   in
   build_newrecursive l'
@@ -321,7 +321,7 @@ let generate_principle  on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-	let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
+	let f_R_mut = Ident (Loc.ghost,mk_rel_id (List.nth names 0)) in
 	let ind_kn =
 	  fst (locate_with_msg
 		 (pr_reference f_R_mut++str ": Not an inductive type!")
@@ -363,7 +363,7 @@ let generate_principle  on_error
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
-      let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
+      let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
 	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
@@ -397,8 +397,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let unbounded_eq =
     let f_app_args =
       Constrexpr.CAppExpl
-	(dummy_loc,
-	 (None,(Ident (dummy_loc,fname))) ,
+	(Loc.ghost,
+	 (None,(Ident (Loc.ghost,fname))) ,
 	 (List.map
 	    (function
 	       | _,Anonymous -> assert false
@@ -408,7 +408,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Constrexpr.CApp (dummy_loc,(None,Constrexpr_ops.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
+    Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
@@ -465,13 +465,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
-	    Libnames.Qualid (dummy_loc,Libnames.qualid_of_path
+	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
 	  in
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
-	    Constrexpr_ops.mkLambdaC ([(dummy_loc,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+	    Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
 	  in
 	  let wf_rel_from_mes =
 	    Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -482,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let a = Names.id_of_string "___a" in 
 	    let b = Names.id_of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
-	      [dummy_loc,Name a;dummy_loc,Name b],
+	      [Loc.ghost,Name a;Loc.ghost,Name b],
 	      Constrexpr.Default Explicit,
 	      wf_arg_type,
 	      Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -590,12 +590,12 @@ let rec rebuild_bl (aux,assoc) bl typ =
 		(if new_nal' = [] && rest = []
 		 then  typ' 
 		 else if new_nal' = [] 
-		 then CProdN(dummy_loc,rest,typ')
-		 else CProdN(dummy_loc,((new_nal',bk',nal't)::rest),typ'))
+		 then CProdN(Loc.ghost,rest,typ')
+		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
 	      let captured_nal,non_captured_nal = list_chop lnal' nal in 
 	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
-		bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ'))
+		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
 
 let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
@@ -628,7 +628,7 @@ let do_generate_principle on_error register_built interactive_proof
 	      | _ -> assert false
 	  in 
 	  let fixpoint_exprl = [fixpoint_expr] in 
-	  let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in 
 	  let pre_hook =
@@ -652,7 +652,7 @@ let do_generate_principle on_error register_built interactive_proof
 	  let fixpoint_exprl = [fixpoint_expr] in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in
-	  let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	  let pre_hook =
 	    generate_principle
 	      on_error
@@ -701,7 +701,7 @@ let rec add_args id new_args b =
   | CRef r ->
       begin      match r with
 	| Libnames.Ident(loc,fname) when fname = id ->
-	    CAppExpl(dummy_loc,(None,r),new_args)
+	    CAppExpl(Loc.ghost,(None,r),new_args)
 	| _ -> b
       end
   | CFix  _  | CCoFix _ -> anomaly "add_args : todo"
@@ -789,7 +789,7 @@ let rec chop_n_arrow n t =
 		      aux (n - nal_l) nal_ta'
 		    else
 		      let new_t' =
-			Constrexpr.CProdN(dummy_loc,
+			Constrexpr.CProdN(Loc.ghost,
 					((snd (list_chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
@@ -867,14 +867,14 @@ let make_graph (f_ref:global_reference) =
 			    )
 			in
 			let b' = add_args (snd id) new_args b in
-			(((id, ( Some (dummy_loc,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+			(((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
 		 let id = id_of_label (con_label c) in
-		 [((dummy_loc,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 do_generate_principle error_error false false expr_list;
 	 (* We register the infos *)
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index bb3071782..56fc9bd2c 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -17,7 +17,7 @@ val functional_induction :
   bool ->
   Term.constr ->
   (Term.constr * Term.constr bindings) option ->
-  intro_pattern_expr Pp.located option ->
+  intro_pattern_expr Loc.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8443959b4..ff62a5c38 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -113,7 +113,7 @@ let list_add_set_eq eq_fun x l =
 
 let const_of_id id =
   let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Pp.dummy_loc,id))
+    qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Nametab.locate_constant princ_ref
   with Not_found -> Errors.error ("cannot find "^ string_of_id id)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7745996c5..d8f999ec5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -274,7 +274,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> dummy_loc, IntroIdentifier id)
+	     (fun id -> Loc.ghost, IntroIdentifier id)
 	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
@@ -459,7 +459,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (*(dummy_loc,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid
+	     (*(Loc.ghost,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
@@ -469,7 +469,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (*(dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid)
+	     (*(Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -538,13 +538,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> dummy_loc, Genarg.IntroIdentifier id)
+	     (fun id -> Loc.ghost, Genarg.IntroIdentifier id)
 	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
     (* before building the full intro pattern for the principle *)
-    let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
+    let pat = Some (Loc.ghost,Genarg.IntroOrAndPattern intro_pats) in
     let eq_ind = Coqlib.build_coq_eq () in
     let eq_construct = mkConstruct((destInd eq_ind),1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
@@ -682,7 +682,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (dummy_loc,Glob_term.NamedHyp id,p)::bindings,id::avoid
+	     (Loc.ghost,Glob_term.NamedHyp id,p)::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
@@ -692,7 +692,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid)
+	     (Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index af7506103..03aee3068 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = CRef (Libnames.Ident (dummy_loc,id)) in
+    let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
     let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
     true
   with _ -> false
@@ -517,16 +517,16 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
     | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
         let _ = prstr "\nICI1!\n";Pp.flush_all() in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args)
+        GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
     | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
     | GLetIn(_,nme,bdy,trm) , _ ->
         let _ = prstr "\nICI2!\n";Pp.flush_all() in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        GLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
         let _ = prstr "\nICI3!\n";Pp.flush_all() in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        GLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
            raise NoMerge
 
@@ -535,16 +535,16 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
   match c1 , c2 with
     | GApp(_,f1, arr1), GApp(_,f2,arr2) ->
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args)
+        GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
     | GLetIn(_,nme,bdy,trm) , _ ->
         let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        GLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
         let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        GLetIn(dummy_loc,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
 
 
@@ -831,7 +831,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = glob_constr_to_constr_expr tp in
-        LocalRawAssum ([(dummy_loc,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
+        LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) concl in
   let arity,_ =
@@ -839,7 +839,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
       (fun (acc,env) (nm,_,c) ->
         let typ = Constrextern.extern_constr false env c in
         let newenv = Environ.push_rel (nm,None,c) env in
-        CProdN (dummy_loc, [[(dummy_loc,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+        CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
@@ -853,12 +853,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     (rawlist:(identifier * glob_constr) list) =
-  let lident = dummy_loc, shift.ident in
+  let lident = Loc.ghost, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
   let lcstor_expr : (bool * (lident * constr_expr)) list  =
     List.map (* zeta_normalize t ? *)
-      (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t))
+      (fun (id,t) -> false, ((Loc.ghost,id),glob_constr_to_constr_expr t))
       rawlist in
   lident , bindlist , Some cstr_expr , lcstor_expr
 
@@ -868,7 +868,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] [] t in
-        GProd (dummy_loc,nme,Explicit,traw,t2)
+        GProd (Loc.ghost,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
@@ -878,7 +878,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] [] t in
-        GProd (dummy_loc,nme,Explicit,traw,t2)
+        GProd (Loc.ghost,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
@@ -915,7 +915,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
 (* Find infos on identifier id. *)
 let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
   let kn_of_id x =
-    let f_ref = Libnames.Ident (dummy_loc,x) in
+    let f_ref = Libnames.Ident (Loc.ghost,x) in
     locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fe359f08d..af7ec6f20 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -189,7 +189,7 @@ let simpl_iter clause =
 (* Others ugly things ... *)
 let (value_f:constr list -> global_reference -> constr) =
   fun al fterm ->
-    let d0 = dummy_loc in
+    let d0 = Loc.ghost in
     let rev_x_id_l =
       (
 	List.fold_left
@@ -861,8 +861,8 @@ let rec make_rewrite_list expr_info max = function
 	  general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
-	     ExplicitBindings[dummy_loc,NamedHyp def,
-			      expr_info.f_constr;dummy_loc,NamedHyp k,
+	     ExplicitBindings[Loc.ghost,NamedHyp def,
+			      expr_info.f_constr;Loc.ghost,NamedHyp k,
 			      (f_S max)]) false g) )
       )
       [make_rewrite_list expr_info max l;
@@ -888,8 +888,8 @@ let make_rewrite expr_info l hp max =
 	   (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
-	     ExplicitBindings[dummy_loc,NamedHyp def,
-			      expr_info.f_constr;dummy_loc,NamedHyp k,
+	     ExplicitBindings[Loc.ghost,NamedHyp def,
+			      expr_info.f_constr;Loc.ghost,NamedHyp k,
 			      (f_S (f_S max))]) false) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
@@ -1279,7 +1279,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     Errors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
-      let na_ref = Libnames.Ident (dummy_loc,na) in
+      let na_ref = Libnames.Ident (Loc.ghost,na) in
       let na_global = Nametab.global na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
@@ -1512,7 +1512,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in 
+    let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in 
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 9698ca73a..87c9e1097 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,8 +13,8 @@ open Tacexpr
 open Quote
 
 let make_cont k x =
-  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in
-  let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
+  let k = TacDynamic(Loc.ghost, Tacinterp.tactic_in (fun _ -> k)) in
+  let x = TacDynamic(Loc.ghost, Pretyping.constr_in x) in
   let tac = <:tactic<let cont := $k in cont $x>> in
   Tacinterp.interp tac
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 9b569a2b6..fea571f2e 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -136,18 +136,18 @@ END;;*)
 (*
 let closed_term_ast l =
   TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
   [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t"));
    Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
 *)
 let closed_term_ast l =
-  let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in
+  let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None);
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
+  [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,id_of_string"t"),None);
    Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
 (*
-let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
+let _ = add_tacdef false ((Loc.ghost,id_of_string"ring_closed_term"
 *)
 
 (****************************************************************************)
@@ -168,14 +168,14 @@ let decl_constant na c =
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, id_of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
+  TacLetIn(false,[(Loc.ghost,id_of_string x),e1],e2)
 
 let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) =
   Tacinterp.eval_tactic
@@ -185,7 +185,7 @@ let ltac_record flds =
   TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds)
 
 
-let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
+let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
 
 let dummy_goal env =
   let (gl,_,sigma) = 
@@ -627,24 +627,24 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
     | None ->
         (match rk, opp, kind with
             Abstract, None, _ ->
-              let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
+              let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morphN) in
+              TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul]))
           | Abstract, Some opp, Some _ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphZ) in
+              TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp]))
           | Abstract, Some opp, None ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
+              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphNword) in
               TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp]))
           | Computational _,_,_ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;zero;one]))
           | Morphism mth,_,_ ->
               let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
+                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
   let t = Retyping.get_type_of env Evd.empty c in
@@ -660,8 +660,8 @@ let interp_power env pow =
   let carrier = Lazy.force coq_hypo in
   match pow with
   | None ->
-      let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+      let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
+      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), lapp coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index b2e2e5b19..17dd563f7 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -80,4 +80,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+    ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5a355b971..2fb8ce451 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -75,4 +75,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,["Coq";"Init";"Datatypes"])
     nat_of_int
-    ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true)
+    ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index b67cbb934..97753951a 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -144,7 +144,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([GRef (Pp.dummy_loc, int31_construct)],
+  ([GRef (Loc.ghost, int31_construct)],
    uninterp_int31,
    true)
 
@@ -258,7 +258,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if less_than i (add_1 n_inlined) then
-      GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i))
+      GRef (Loc.ghost, bigN_constructor i)::(build (add_1 i))
     else
       []
   in
@@ -304,8 +304,8 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([GRef (Pp.dummy_loc, bigZ_pos);
-    GRef (Pp.dummy_loc, bigZ_neg)],
+  ([GRef (Loc.ghost, bigZ_pos);
+    GRef (Loc.ghost, bigZ_neg)],
    uninterp_bigZ,
    true)
 
@@ -325,5 +325,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ,
+  ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f8161c52f..4e0a206dd 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -118,8 +118,8 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([GRef(dummy_loc,glob_Ropp);GRef(dummy_loc,glob_R0);
-    GRef(dummy_loc,glob_Rplus);GRef(dummy_loc,glob_Rmult);
-    GRef(dummy_loc,glob_R1)],
+  ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0);
+    GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult);
+    GRef(Loc.ghost,glob_R1)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index ac17492d2..7474a8b0e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -64,6 +64,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([GRef (dummy_loc,static_glob_String);
-      GRef (dummy_loc,static_glob_EmptyString)],
+    ([GRef (Loc.ghost,static_glob_String);
+      GRef (Loc.ghost,static_glob_EmptyString)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index a69ec9ed1..e461ea152 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -87,9 +87,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([GRef (dummy_loc, glob_xI);
-    GRef (dummy_loc, glob_xO);
-    GRef (dummy_loc, glob_xH)],
+  ([GRef (Loc.ghost, glob_xI);
+    GRef (Loc.ghost, glob_xO);
+    GRef (Loc.ghost, glob_xH)],
    uninterp_positive,
    true)
 
@@ -138,8 +138,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([GRef (dummy_loc, glob_N0);
-    GRef (dummy_loc, glob_Npos)],
+  ([GRef (Loc.ghost, glob_N0);
+    GRef (Loc.ghost, glob_Npos)],
   uninterp_n,
   true)
 
@@ -186,8 +186,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (dummy_loc, glob_ZERO);
-    GRef (dummy_loc, glob_POS);
-    GRef (dummy_loc, glob_NEG)],
+  ([GRef (Loc.ghost, glob_ZERO);
+    GRef (Loc.ghost, glob_POS);
+    GRef (Loc.ghost, glob_NEG)],
   uninterp_z,
   true)