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, 77 insertions, 69 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e9a852455d..91e1cd5acc 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -100,7 +100,7 @@ let print_rewrite_hintdb bas =
 	       Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
 	   (find_rewrites bas))
 
-type raw_rew_rule = loc * constr * bool * raw_tactic_expr
+type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index e5ec949ed4..6bd8e1536e 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Tacmach
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Pp.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -56,6 +56,6 @@ type hypinfo = {
 }
 
 val find_applied_relation : bool ->
-  Pp.loc ->
+  Loc.t ->
   Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c8fe1a4267..6557e52ab1 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -37,7 +37,6 @@ open Pfedit
 open Command
 open Globnames
 open Evd
-open Compat
 open Locus
 open Misctypes
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 76ee9ff680..a817efc33f 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -23,7 +23,7 @@ open Misctypes
 
 let absurd c gls =
   let env = pf_env gls and sigma = project gls in
-  let _,j = Coercion.inh_coerce_to_sort dummy_loc env
+  let _,j = Coercion.inh_coerce_to_sort Loc.ghost env
     (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
   let c = j.Environ.utj_val in
   (tclTHENS
diff --git a/tactics/elim.mli b/tactics/elim.mli
index fe19c0b245..ab2d4ad5ef 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -20,7 +20,7 @@ val introElimAssumsThen :
   (branch_assumptions -> tactic) -> branch_args -> tactic
 
 val introCaseAssumsThen :
-  (intro_pattern_expr Pp.located list -> branch_assumptions -> tactic) ->
+  (intro_pattern_expr Loc.located list -> branch_assumptions -> tactic) ->
     branch_args -> tactic
 
 val general_decompose : (identifier * constr -> bool) -> constr -> tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 81457fc9ca..f7e7361d51 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1147,7 +1147,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
               then (
 (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
               let qidl = qualid_of_reference
-                (Ident (dummy_loc,id_of_string "Eqdep_dec")) in
+                (Ident (Loc.ghost,id_of_string "Eqdep_dec")) in
               Library.require_library [qidl] (Some false);
 (* cut with the good equality and prove the requested goal *)
               tclTHENS (cut (mkApp (ceq,new_eq_args)) )
@@ -1170,7 +1170,7 @@ let injClause ipats with_evars = function
   | Some c -> onInductionArg (inj ipats with_evars) c
 
 let injConcl gls  = injClause [] false None gls
-let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
+let injHyp id gls = injClause [] false (Some (ElimOnIdent (Loc.ghost,id))) gls
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index cd04181c02..c7ac346976 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,9 +91,9 @@ val discrHyp     : identifier -> tactic
 val discrEverywhere : evars_flag -> tactic
 val discr_tac    : evars_flag ->
   constr with_bindings induction_arg option -> tactic
-val inj          : intro_pattern_expr located list -> evars_flag ->
+val inj          : intro_pattern_expr Loc.located list -> evars_flag ->
   constr with_bindings -> tactic
-val injClause    : intro_pattern_expr located list -> evars_flag ->
+val injClause    : intro_pattern_expr Loc.located list -> evars_flag ->
   constr with_bindings induction_arg option -> tactic
 val injHyp       : identifier -> tactic
 val injConcl     : tactic
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 4b5229010f..1b5c2d6d09 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -52,7 +52,7 @@ let instantiate n (ist,rawc) ido gl =
         gl
 
 let let_evar name typ gls =
-  let src = (dummy_loc,Evar_kinds.GoalEvar) in
+  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in
   Refiner.tclTHEN (Refiner.tclEVARS sigma')
     (Tactics.letin_tac None name evar None Locusops.nowhere) gls
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index bff4f47601..7bfda9802c 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -125,7 +125,7 @@ END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = identifier Pp.located gen_place
+type loc_place = identifier Loc.located gen_place
 type place = identifier gen_place
 
 let pr_gen_place pr_id = function
@@ -167,11 +167,11 @@ ARGUMENT EXTEND hloc
   |  [ "in" "|-" "*" ] ->
     [ ConclLocation () ]
 | [ "in" ident(id) ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHyp) ]
+    [ HypLocation ((Loc.ghost,id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHypTypeOnly) ]
+    [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHypValueOnly) ]
+    [ HypLocation ((Loc.ghost,id),InHypValueOnly) ]
 
  END
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index ee4f38c9d7..60ee03f0ec 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -33,7 +33,7 @@ val glob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
-type loc_place = identifier Pp.located gen_place
+type loc_place = identifier Loc.located gen_place
 type place = identifier gen_place
 
 val rawwit_hloc : loc_place raw_abstract_argument_type
@@ -41,11 +41,11 @@ val wit_hloc : place typed_abstract_argument_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
-val in_arg_hyp:  (Names.identifier Pp.located list option * bool)  Pcoq.Gram.entry
-val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type
-val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type
+val in_arg_hyp:  (Names.identifier Loc.located list option * bool)  Pcoq.Gram.entry
+val globwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) glob_abstract_argument_type
+val rawwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) raw_abstract_argument_type
 val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
-val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Locus.clause
+val raw_in_arg_hyp_to_clause : (Names.identifier Loc.located list option * bool) -> Locus.clause
 val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Locus.clause
 val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8abb9c9e4e..c414339ff8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -22,7 +22,6 @@ open Errors
 open Util
 open Evd
 open Equality
-open Compat
 open Misctypes
 
 (**********************************************************************)
@@ -67,7 +66,7 @@ END
 
 let induction_arg_of_quantified_hyp = function
   | AnonHyp n -> ElimOnAnonHyp n
-  | NamedHyp id -> ElimOnIdent (Pp.dummy_loc,id)
+  | NamedHyp id -> ElimOnIdent (Loc.ghost,id)
 
 (* Versions *_main must come first!! so that "1" is interpreted as a
    ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
@@ -558,7 +557,7 @@ let subst_var_with_hole occ tid t =
 	   if !occref = 0 then x
            else
 	     (incr locref;
-	      GHole (make_loc (!locref,0),
+	      GHole (Loc.make_loc (!locref,0),
 		     Evar_kinds.QuestionMark(Evar_kinds.Define true))))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -575,7 +574,7 @@ let subst_hole_with_term occ tc t =
         if !occref = 0 then tc
         else
 	  (incr locref;
-	   GHole (make_loc (!locref,0),
+	   GHole (Loc.make_loc (!locref,0),
 		  Evar_kinds.QuestionMark(Evar_kinds.Define true)))
     | c -> map_glob_constr_left_to_right substrec c
   in
@@ -599,7 +598,7 @@ let hResolve id c occ t gl =
       Pretyping.understand sigma env t_hole
     with 
     | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) ->
-        resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
+        resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index d1d3d90c5c..d5ee78feaf 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -64,10 +64,10 @@ let h_generalize cl =
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
 let h_let_tac b na c cl =
-  let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in
+  let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl)
 let h_let_pat_tac b na c cl =
-  let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in
+  let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,snd c,cl,b))
     (letin_pat_tac with_eq na c None cl)
 
@@ -132,8 +132,8 @@ let h_transitivity c =
   abstract_tactic (TacTransitivity c)
     (intros_transitivity c)
 
-let h_simplest_apply c = h_apply false false [Pp.dummy_loc,(c,NoBindings)]
-let h_simplest_eapply c = h_apply false true [Pp.dummy_loc,(c,NoBindings)]
+let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)]
+let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index af7a2061b7..cffe84252e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Names
 open Pp
 open Term
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 7dc9feb2c7..05ba0e576d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index fc72bd4e46..16e0b958f6 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -1,3 +1,12 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
 open Pp
 open Names
 open Term
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 867fea08c5..1807839835 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -39,7 +39,6 @@ open Command
 open Libnames
 open Globnames
 open Evd
-open Compat
 open Misctypes
 open Locus
 open Locusops
@@ -55,10 +54,10 @@ let init_setoid () =
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
 
 let proper_class =
-  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Proper"))))
+  lazy (class_info (Nametab.global (Qualid (Loc.ghost, qualid_of_string "Coq.Classes.Morphisms.Proper"))))
 
 let proper_proxy_class =
-  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy"))))
+  lazy (class_info (Nametab.global (Qualid (Loc.ghost, qualid_of_string "Coq.Classes.Morphisms.ProperProxy"))))
 
 let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
 
@@ -150,7 +149,7 @@ let build_signature evars env m (cstrs : (types * types option) option list)
     (finalcstr : (types * types option) option) =
   let new_evar evars env t =
     new_cstr_evar evars env
-      (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
+      (* ~src:(Loc.ghost, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
   let mk_relty evars env ty obj =
     match obj with
@@ -1478,33 +1477,33 @@ TACTIC EXTEND GenRew
     [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
 END
 
-let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
+let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,id_of_string s))),l)
 
 let declare_an_instance n s args =
-  ((dummy_loc,Name n), Explicit,
-  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)),
+  ((Loc.ghost,Name n), Explicit,
+  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s)),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
-  new_instance binders instance (Some (CRecord (dummy_loc,None,fields)))
+  new_instance binders instance (Some (CRecord (Loc.ghost,None,fields)))
     ~global:(not (Locality.use_section_locality ())) ~generalize:false None
 
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance global binders instance
-       [(Ident (dummy_loc,id_of_string "reflexivity"),lemma)]
+       [(Ident (Loc.ghost,id_of_string "reflexivity"),lemma)]
 
 let declare_instance_sym global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance global binders instance
-       [(Ident (dummy_loc,id_of_string "symmetry"),lemma)]
+       [(Ident (Loc.ghost,id_of_string "symmetry"),lemma)]
 
 let declare_instance_trans global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance global binders instance
-       [(Ident (dummy_loc,id_of_string "transitivity"),lemma)]
+       [(Ident (Loc.ghost,id_of_string "transitivity"),lemma)]
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
@@ -1528,16 +1527,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
-	       (Ident (dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)])
+	      [(Ident (Loc.ghost,id_of_string "PreOrder_Reflexive"), lemma1);
+	       (Ident (Loc.ghost,id_of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (dummy_loc,id_of_string "PER_Symmetric"), lemma2);
-	       (Ident (dummy_loc,id_of_string "PER_Transitive"),lemma3)])
+	      [(Ident (Loc.ghost,id_of_string "PER_Symmetric"), lemma2);
+	       (Ident (Loc.ghost,id_of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1545,9 +1544,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance global binders instance
-	    [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
-	     (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
-	     (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
+	    [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), lemma1);
+	     (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), lemma2);
+	     (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), lemma3)])
 
 type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1626,7 +1625,7 @@ VERNAC COMMAND EXTEND AddParametricRelation3
       [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
 
-let cHole = CHole (dummy_loc, None)
+let cHole = CHole (Loc.ghost, None)
 
 open Entries
 open Libnames
@@ -1723,9 +1722,9 @@ let add_setoid global binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance global binders instance
-      [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 let add_morphism_infer glob m n =
   init_setoid ();
@@ -1754,13 +1753,13 @@ let add_morphism glob binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance =
-    ((dummy_loc,Name instance_id), Explicit,
-    CAppExpl (dummy_loc,
-	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
+    ((Loc.ghost,Name instance_id), Explicit,
+    CAppExpl (Loc.ghost,
+	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-    ignore(new_instance ~global:glob binders instance (Some (CRecord (dummy_loc,None,[])))
+    ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[])))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
 VERNAC COMMAND EXTEND AddSetoid1
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 45e48a9d78..2beba9888b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -51,7 +51,6 @@ open Syntax_def
 open Pretyping
 open Extrawit
 open Pcoq
-open Compat
 open Evd
 open Misctypes
 open Miscops
@@ -95,7 +94,7 @@ type value =
   | VList of value list
   | VRec of (identifier*value) list ref * glob_tactic_expr
 
-let dloc = dummy_loc
+let dloc = Loc.ghost
 
 let catch_error call_trace tac g =
   if call_trace = [] then tac g else try tac g with
@@ -156,7 +155,7 @@ let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t),
 let ((value_in : value -> Dyn.t),
      (value_out : Dyn.t -> value)) = Dyn.create "value"
 
-let valueIn t = TacDynamic (dummy_loc,value_in t)
+let valueIn t = TacDynamic (Loc.ghost,value_in t)
 let valueOut = function
   | TacDynamic (_,d) ->
     if (Dyn.tag d) = "value" then
@@ -1547,14 +1546,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
   sigma, (c, bl)
 
 let loc_of_bindings = function
-| NoBindings -> dummy_loc
+| NoBindings -> Loc.ghost
 | ImplicitBindings l -> loc_of_glob_constr (fst (list_last l))
 | ExplicitBindings l -> pi1 (list_last l)
 
 let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
-  let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in
+  let loc = if loc2 = Loc.ghost then loc1 else Loc.merge loc1 loc2 in
   let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
   sigma, (loc,cb)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index d1fe9de115..7ce0d3f842 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -104,7 +104,7 @@ val intern_constr_with_bindings :
   glob_constr_and_expr * glob_constr_and_expr bindings
 
 val intern_hyp :
-  glob_sign -> identifier Pp.located -> identifier Pp.located
+  glob_sign -> identifier Loc.located -> identifier Loc.located
 
 val subst_genarg :
   substitution -> glob_generic_argument -> glob_generic_argument
@@ -129,7 +129,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 val interp_tac_gen : (identifier * value) list -> identifier list ->
                  debug_info -> raw_tactic_expr -> tactic
 
-val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
+val interp_hyp :  interp_sign -> goal sigma -> identifier Loc.located -> identifier
 
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
@@ -165,8 +165,8 @@ val print_ltac : Libnames.qualid -> std_ppcmds
 
 exception CannotCoerceTo of string
 
-val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier located -> 'a
+val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier Loc.located -> 'a
 
-val interp_int : interp_sign -> identifier located -> int
+val interp_int : interp_sign -> identifier Loc.located -> int
 
-val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a
+val error_ltac_variable : Loc.t -> identifier -> Environ.env option -> value -> string -> 'a
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4ba26dcebc..6640007971 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -174,7 +174,7 @@ type branch_args = {
   nassums    : int;         (* the number of assumptions to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=recursive argument, false=constant *)
-  branchnames : intro_pattern_expr located list}
+  branchnames : intro_pattern_expr Loc.located list}
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3c1beda400..d369109ed9 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term
@@ -126,7 +127,7 @@ type branch_assumptions = {
 (** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
    error message if |pats| <> n *)
 val check_or_and_pattern_size :
-  Pp.loc -> or_and_intro_pattern_expr -> int -> unit
+  Loc.t -> or_and_intro_pattern_expr -> int -> unit
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
 val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f386def1f..0d32ed46f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Pp
 open Errors
 open Util
@@ -61,7 +60,7 @@ let rec nb_prod x =
 
 let inj_with_occurrences e = (AllOccurrences,e)
 
-let dloc = dummy_loc
+let dloc = Loc.ghost
 
 let typ_of = Retyping.get_type_of
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2cbefb8178..6cdac9d557 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term