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

5 files changed, 21 insertions, 17 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 87815dc0b..bdf69c9cf 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -104,7 +104,7 @@ let pr_com_at n =
   if Flags.do_beautify() && n <> 0 then comment n
   else mt()
 
-let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+let pr_with_comments loc pp = Loc.pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
@@ -137,14 +137,14 @@ let pr_opt_type_spc pr = function
   | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
 let pr_lident (loc,id) =
-  if loc <> dummy_loc then
-    let (b,_) = unloc loc in
-    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+  if loc <> Loc.ghost then
+    let (b,_) = Loc.unloc loc in
+    Loc.pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
 
 let pr_lname = function
     (loc,Name id) -> pr_lident (loc,id)
-  | lna -> pr_located pr_name lna
+  | lna -> Loc.pr_located pr_name lna
 
 let pr_or_var pr = function
   | ArgArg x -> pr x
@@ -213,8 +213,8 @@ let pr_eqn pr (loc,pl,rhs) =
       pr_sep_com spc (pr ltop) rhs))
 
 let begin_of_binder = function
-    LocalRawDef((loc,_),_) -> fst (unloc loc)
-  | LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc)
+    LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
+  | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
   | _ -> assert false
 
 let begin_of_binders = function
@@ -260,7 +260,7 @@ let pr_binder_among_many pr_c = function
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, (CastConv t|CastVM t)) -> c, t
-        | _ -> c, CHole (dummy_loc, None) in
+        | _ -> c, CHole (Loc.ghost, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 304e5958e..598bb3ed3 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Environ
 open Term
@@ -34,7 +35,7 @@ val pr_metaid : identifier -> std_ppcmds
 val pr_lident : identifier located -> std_ppcmds
 val pr_lname : name located -> std_ppcmds
 
-val pr_with_comments : loc -> std_ppcmds -> std_ppcmds
+val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
 val pr_com_at : int -> std_ppcmds
 val pr_sep_com :
   (unit -> std_ppcmds) ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 14cfe2ffc..815ee6e5c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -357,7 +357,7 @@ let pr_as_ipat = function
 
 let pr_as_name = function
   | Anonymous -> mt ()
-  | Name id -> str " as " ++ pr_lident (dummy_loc,id)
+  | Name id -> str " as " ++ pr_lident (Loc.ghost,id)
 
 let pr_pose_as_style prc na c =
   spc() ++ prc c ++ pr_as_name na
@@ -479,7 +479,7 @@ let pr_funvar = function
 
 let pr_let_clause k pr (id,(bl,t)) =
   hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
-         str " :=" ++ brk (1,1) ++ pr (TacArg (dummy_loc,t)))
+         str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
 
 let pr_let_clauses recflag pr = function
   | hd::tl ->
@@ -952,7 +952,7 @@ and pr_tacarg = function
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
       spc() ++ prlist_with_sep spc pr_tacarg la
   | (TacCall _|Tacexp _|Integer _) as a ->
-      str "ltac:" ++ pr_tac (latom,E) (TacArg (dummy_loc,a))
+      str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
 
 in (pr_tac, pr_match_rule)
 
@@ -961,7 +961,7 @@ let strip_prod_binders_glob_constr n (ty,_) =
     if n=0 then (List.rev acc, (ty,None)) else
       match ty with
           Glob_term.GProd(loc,na,Explicit,a,b) ->
-            strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
+            strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
@@ -970,7 +970,7 @@ let strip_prod_binders_constr n ty =
     if n=0 then (List.rev acc, ty) else
       match Term.kind_of_term ty with
           Term.Prod(na,a,b) ->
-            strip_ty (([dummy_loc,na],a)::acc) (n-1) b
+            strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 07838edcd..efca60f00 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -10,6 +10,9 @@ open Pp
 open Names
 open Nameops
 open Nametab
+
+let pr_located = Loc.pr_located
+
 open Compat
 open Errors
 open Util
@@ -30,7 +33,7 @@ open Declaremods
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
 let pr_lident (loc,id) =
-  if loc <> dummy_loc then
+  if loc <> Loc.ghost then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
@@ -41,7 +44,7 @@ let string_of_fqid fqid =
 let pr_fqid fqid = str (string_of_fqid fqid)
 
 let pr_lfqid (loc,fqid) =
-  if loc <> dummy_loc then
+  if loc <> Loc.ghost then
    let (b,_) = unloc loc in
     pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
   else
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2e8cc4023..5e65bde25 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp =
 let gallina_print_syntactic_def kn =
   let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
-  let c = Notation_ops.glob_constr_of_notation_constr dummy_loc a in
+  let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in
   hov 2
     (hov 4
        (str "Notation " ++ pr_qualid qid ++