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

1 files changed, 4 insertions, 5 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 45e48a9d7..2beba9888 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)