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

10 files changed, 90 insertions, 90 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 169f4d1204..9fcfeb36c9 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 7b341e581b..93e1d105e6 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 8967a3ec85..f678b898ba 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 437ba225d6..9cf83df152 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 2a6a7dea32..5b9bf44c3b 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 bb3071782e..56fc9bd2cd 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 8443959b4b..ff62a5c385 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 7745996c58..d8f999ec54 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 af7506103d..03aee30685 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 fe359f08d9..af7ec6f207 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);