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

12 files changed, 30 insertions, 29 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 323da812de..98fd215ae5 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -65,7 +65,7 @@ type grammar_constr_prod_item =
        concat with last parsed list if true *)
 
 let make_constr_action
-  (f : loc -> constr_notation_substitution -> constr_expr) pil =
+  (f : Loc.t -> constr_notation_substitution -> constr_expr) pil =
   let rec make (constrs,constrlists,binders as fullsubst) = function
   | [] ->
       Gram.action (fun loc -> f loc fullsubst)
@@ -82,11 +82,11 @@ let make_constr_action
         Gram.action (fun (v:reference) ->
 	  make (CRef v :: constrs, constrlists, binders) tl)
     | ETName ->
-        Gram.action (fun (na:name located) ->
+        Gram.action (fun (na:Loc.t * name) ->
 	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
+	  make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl)
     | ETConstrList (_,n) ->
 	Gram.action (fun (v:constr_expr list) ->
 	  make (constrs, v::constrlists, binders) tl)
@@ -113,7 +113,7 @@ let check_cases_pattern_env loc (env,envlist,hasbinders) =
   else (env,envlist)
 
 let make_cases_pattern_action
-  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
+  (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
   let rec make (env,envlist,hasbinders as fullenv) = function
   | [] ->
       Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
@@ -128,13 +128,13 @@ let make_cases_pattern_action
           make (v::env, envlist, hasbinders) tl)
     | ETReference ->
         Gram.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
+	  make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl)
     | ETName ->
-        Gram.action (fun (na:name located) ->
+        Gram.action (fun (na:Loc.t * name) ->
 	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
+	  make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl)
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
 	  make (env, vl :: envlist, hasbinders) tl)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 62e7ae2bbf..e86f3b385e 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
 (** Making generic actions in type generic_argument *)
 
 let make_generic_action
-  (f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
+  (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
   let rec make env = function
     | [] ->
 	Gram.action (fun loc -> f loc env)
@@ -37,7 +37,7 @@ let make_rule_gen mkproditem mkact pt =
 type grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal of
-      loc * argument_type * prod_entry_key * identifier option
+      Loc.t * argument_type * prod_entry_key * identifier option
 
 let make_prod_item = function
   | GramTerminal s -> (gram_token_of_string s, None)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 350e75f90c..e379052710 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -13,7 +13,7 @@
 
 type grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal of Pp.loc * Genarg.argument_type *
+  | GramNonTerminal of Loc.t * Genarg.argument_type *
       Pcoq.prod_entry_key * Names.identifier option
 
 val extend_tactic_grammar :
@@ -29,5 +29,5 @@ val get_extend_vernac_grammars :
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
-  (Pp.loc -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) ->
+  (Loc.t -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) ->
   grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f53cab6c68..f92ee43506 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -36,7 +36,7 @@ let _ = List.iter Lexer.add_keyword constr_kw
 let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
-    let loc = join_loc (constr_loc c) (constr_loc ty)
+    let loc = Loc.merge (constr_loc c) (constr_loc ty)
     in CCast(loc, c, CastConv ty)
 
 let binders_of_names l =
@@ -235,7 +235,7 @@ GEXTEND Gram
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let loc1 =
-	    join_loc (local_binders_loc bl) (constr_loc c1)
+	    Loc.merge (local_binders_loc bl) (constr_loc c1)
 	  in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
@@ -422,7 +422,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,c)]
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))]
+          [LocalRawDef (id,CCast (Loc.merge (constr_loc t) loc,c, CastConv t))]
       | "{"; id=name; "}" ->
           [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 437f0e78e5..5da6ddf3de 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -180,7 +180,7 @@ GEXTEND Gram
 	      | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty)
+	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None))) ty)
     ] ]
   ;
   match_context_rule:
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 7d7f2b10d3..3bc26aa6a6 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -46,7 +46,7 @@ open Pcoq
 open Prim
 open Constr
 
-let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
   GLOBAL: withtac;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 927776b4ea..462aa2b469 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -139,7 +139,7 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [([(ElimOnAnonHyp n)],None,(None,None))],None ->
       TacCase (with_evar,
-        (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))),
+        (CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))),
 	 NoBindings))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
@@ -156,17 +156,17 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (join_loc loc1 loc) bll c)
+      CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
   | [] -> c
 
 let mkCLambdaN_simple bl c =
   if bl=[] then c
   else
-    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in
+    let loc = Loc.merge (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
-let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
+let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (list_last l))
 
 let map_int_or_var f = function
   | ArgArg x -> ArgArg (f x)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 445908fba2..fbf1c64f2a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -536,16 +536,16 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Global,CanonicalStructure),(dummy_loc,s),d,
+	    ((Global,CanonicalStructure),(Loc.ghost,s),d,
 	     (fun _ -> Recordops.declare_canonical_structure))
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (enforce_locality_exp true, f, s, t)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 7387f6933f..f3b824e6d1 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -27,8 +27,8 @@ open Genredexpr
 
 (* Generic xml parser without raw data *)
 
-type attribute = string * (loc * string)
-type xml = XmlTag of loc * string * attribute list * xml list
+type attribute = string * (Loc.t * string)
+type xml = XmlTag of Loc.t * string * attribute list * xml list
 
 let check_tags loc otag ctag =
   if otag <> ctag then
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index dba552e77c..fcdaa6eba0 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -538,7 +538,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc
 
 let current_location_table = ref (loct_create ())
 
-type location_table = (int, loc) Hashtbl.t
+type location_table = (int, Loc.t) Hashtbl.t
 let location_table () = !current_location_table
 let restore_location_table t = current_location_table := t
 let location_function n = loct_func !current_location_table n
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 95eadfcb67..66a04a194d 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -12,7 +12,7 @@ val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
-val location_function : int -> loc
+val location_function : int -> Loc.t
 
 (** for coqdoc *)
 type location_table
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 147c5261d9..2e11c1c471 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Glob_term
@@ -171,7 +172,7 @@ module Prim :
     val qualid : qualid located Gram.entry
     val fullyqualid : identifier list located Gram.entry
     val reference : reference Gram.entry
-    val by_notation : (loc * string * string option) Gram.entry
+    val by_notation : (Loc.t * string * string option) Gram.entry
     val smart_global : reference or_by_notation Gram.entry
     val dirpath : dir_path Gram.entry
     val ne_string : string Gram.entry
@@ -242,7 +243,7 @@ module Vernac_ :
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (loc * vernac_expr) option Gram.entry
+val main_entry : (Loc.t * vernac_expr) option Gram.entry
 
 (** Mapping formal entries into concrete ones *)