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

7 files changed, 75 insertions, 74 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 605be512c1..d8387b9df3 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Libnames
@@ -36,27 +37,27 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 type prim_token = Numeral of Bigint.bigint | String of string
 
 type raw_cases_pattern_expr =
-  | RCPatAlias of loc * raw_cases_pattern_expr * identifier
-  | RCPatCstr of loc * Globnames.global_reference
+  | RCPatAlias of Loc.t * raw_cases_pattern_expr * identifier
+  | RCPatCstr of Loc.t * Globnames.global_reference
     * raw_cases_pattern_expr list * raw_cases_pattern_expr list
   (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
-  | RCPatAtom of loc * identifier option
-  | RCPatOr of loc * raw_cases_pattern_expr list
+  | RCPatAtom of Loc.t * identifier option
+  | RCPatOr of Loc.t * raw_cases_pattern_expr list
 
 type cases_pattern_expr =
-  | CPatAlias of loc * cases_pattern_expr * identifier
-  | CPatCstr of loc * reference
+  | CPatAlias of Loc.t * cases_pattern_expr * identifier
+  | CPatCstr of Loc.t * reference
     * cases_pattern_expr list * cases_pattern_expr list
   (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
-  | CPatAtom of loc * reference option
-  | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_notation_substitution
+  | CPatAtom of Loc.t * reference option
+  | CPatOr of Loc.t * cases_pattern_expr list
+  | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
     * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
 				  (notation n applied with substitution l1)
 				  applied to arguments l2 *)
-  | CPatPrim of loc * prim_token
-  | CPatRecord of loc * (reference * cases_pattern_expr) list
-  | CPatDelimiters of loc * string * cases_pattern_expr
+  | CPatPrim of Loc.t * prim_token
+  | CPatRecord of Loc.t * (reference * cases_pattern_expr) list
+  | CPatDelimiters of Loc.t * string * cases_pattern_expr
 
 and cases_pattern_notation_substitution =
     cases_pattern_expr list *     (** for constr subterms *)
@@ -64,31 +65,31 @@ and cases_pattern_notation_substitution =
 
 type constr_expr =
   | CRef of reference
-  | CFix of loc * identifier located * fix_expr list
-  | CCoFix of loc * identifier located * cofix_expr list
-  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
-  | CApp of loc * (proj_flag * constr_expr) *
+  | CFix of Loc.t * identifier located * fix_expr list
+  | CCoFix of Loc.t * identifier located * cofix_expr list
+  | CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
+  | CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
+  | CLetIn of Loc.t * name located * constr_expr * constr_expr
+  | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list
+  | CApp of Loc.t * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (reference * constr_expr) list
-  | CCases of loc * case_style * constr_expr option *
+  | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
+  | CCases of Loc.t * case_style * constr_expr option *
       (constr_expr * (name located option * cases_pattern_expr option)) list *
-      (loc * cases_pattern_expr list located list * constr_expr) list
-  | CLetTuple of loc * name located list * (name located option * constr_expr option) *
+      (Loc.t * cases_pattern_expr list located list * constr_expr) list
+  | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name located option * constr_expr option)
+  | CIf of Loc.t * constr_expr * (name located option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc * Evar_kinds.t option
-  | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * glob_sort
-  | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_notation_substitution
-  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
-  | CPrim of loc * prim_token
-  | CDelimiters of loc * string * constr_expr
+  | CHole of Loc.t * Evar_kinds.t option
+  | CPatVar of Loc.t * (bool * patvar)
+  | CEvar of Loc.t * existential_key * constr_expr list option
+  | CSort of Loc.t * glob_sort
+  | CCast of Loc.t * constr_expr * constr_expr cast_type
+  | CNotation of Loc.t * notation * constr_notation_substitution
+  | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
+  | CPrim of Loc.t * prim_token
+  | CDelimiters of Loc.t * string * constr_expr
 
 and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) *
@@ -126,5 +127,5 @@ type with_declaration_ast =
 
 type module_ast =
   | CMident of qualid located
-  | CMapply of loc * module_ast * module_ast
-  | CMwith of loc * module_ast * with_declaration_ast
+  | CMapply of Loc.t * module_ast * module_ast
+  | CMwith of Loc.t * module_ast * with_declaration_ast
diff --git a/intf/extend.mli b/intf/extend.mli
index 6b29fc7476..3b14ceea96 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
-
 (** Entry keys for constr notations *)
 
 type side = Left | Right
 
 type production_position =
-  | BorderProd of side * gram_assoc option
+  | BorderProd of side * Compat.gram_assoc option
   | InternalProd
 
 type production_level =
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 8aab193fd5..a7e08dbbce 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -44,5 +44,5 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (Pp.loc * Names.identifier) * 'a
+  | ConstrContext of (Loc.t * Names.identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 7ee0320f08..5cb369562d 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -27,31 +27,31 @@ open Misctypes
 
      locs here refers to the ident's location, not whole pat *)
 type cases_pattern =
-  | PatVar of loc * name
-  | PatCstr of loc * constructor * cases_pattern list * name
+  | PatVar of Loc.t * name
+  | PatCstr of Loc.t * constructor * cases_pattern list * name
       (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
 
 type glob_constr =
-  | GRef of (loc * global_reference)
-  | GVar of (loc * identifier)
-  | GEvar of loc * existential_key * glob_constr list option
-  | GPatVar of loc * (bool * patvar) (** Used for patterns only *)
-  | GApp of loc * glob_constr * glob_constr list
-  | GLambda of loc * name * binding_kind *  glob_constr * glob_constr
-  | GProd of loc * name * binding_kind * glob_constr * glob_constr
-  | GLetIn of loc * name * glob_constr * glob_constr
-  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
+  | GRef of (Loc.t * global_reference)
+  | GVar of (Loc.t * identifier)
+  | GEvar of Loc.t * existential_key * glob_constr list option
+  | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
+  | GApp of Loc.t * glob_constr * glob_constr list
+  | GLambda of Loc.t * name * binding_kind *  glob_constr * glob_constr
+  | GProd of Loc.t * name * binding_kind * glob_constr * glob_constr
+  | GLetIn of Loc.t * name * glob_constr * glob_constr
+  | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
 	  [MatchStyle]) *)
 
-  | GLetTuple of loc * name list * (name * glob_constr option) *
+  | GLetTuple of Loc.t * name list * (name * glob_constr option) *
       glob_constr * glob_constr
-  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
-  | GRec of loc * fix_kind * identifier array * glob_decl list array *
+  | GIf of Loc.t * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
+  | GRec of Loc.t * fix_kind * identifier array * glob_decl list array *
       glob_constr array * glob_constr array
-  | GSort of loc * glob_sort
-  | GHole of (loc * Evar_kinds.t)
-  | GCast of loc * glob_constr * glob_constr cast_type
+  | GSort of Loc.t * glob_sort
+  | GHole of (Loc.t * Evar_kinds.t)
+  | GCast of Loc.t * glob_constr * glob_constr cast_type
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
 
@@ -65,14 +65,14 @@ and fix_kind =
   | GCoFix of int
 
 and predicate_pattern =
-    name * (loc * inductive * name list) option
+    name * (Loc.t * inductive * name list) option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
 
 and tomatch_tuples = tomatch_tuple list
 
-and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
+and cases_clause = (Loc.t * identifier list * cases_pattern list * glob_constr)
 (** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *)
 
 and cases_clauses = cases_clause list
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index a511458129..b9f5a6dbe2 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -25,7 +25,7 @@ type intro_pattern_expr =
   | IntroFresh of identifier
   | IntroForthcoming of bool
   | IntroAnonymous
-and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list
+and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
 
 (** Move destination for hypothesis *)
 
@@ -52,7 +52,7 @@ type 'a cast_type =
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
-type 'a explicit_bindings = (Pp.loc * quantified_hypothesis * 'a) list
+type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list
 
 type 'a bindings =
   | ImplicitBindings of 'a list
@@ -66,13 +66,13 @@ type 'a with_bindings = 'a * 'a bindings
 
 type 'a or_var =
   | ArgArg of 'a
-  | ArgVar of Names.identifier Pp.located
+  | ArgVar of Names.identifier Loc.located
 
-type 'a and_short_name = 'a * identifier Pp.located option
+type 'a and_short_name = 'a * identifier Loc.located option
 
 type 'a or_by_notation =
   | AN of 'a
-  | ByNotation of (Pp.loc * string * string option)
+  | ByNotation of (Loc.t * string * string option)
 
 (* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
    but this formulation avoids a useless dependency. *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 895eca2d95..ccf682a48e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Names
 open Constrexpr
 open Libnames
@@ -19,7 +20,7 @@ open Misctypes
 open Locus
 open Pp
 
-type 'a or_metaid = AI of 'a | MetaId of loc * string
+type 'a or_metaid = AI of 'a | MetaId of Loc.t * string
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
@@ -154,15 +155,15 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
 
   (* For ML extensions *)
-  | TacExtend of loc * string * 'lev generic_argument list
+  | TacExtend of Loc.t * string * 'lev generic_argument list
 
   (* For syntax extensions *)
-  | TacAlias of loc * string *
+  | TacAlias of Loc.t * string *
       (identifier * 'lev generic_argument) list
       * (dir_path * glob_tactic_expr)
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
-  | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr
+  | TacAtom of Loc.t * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr
   | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array *
 	('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
@@ -193,16 +194,16 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast =
 
   (* These are the possible arguments of a tactic definition *)
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
-  | TacDynamic     of loc * Dyn.t
+  | TacDynamic     of Loc.t * Dyn.t
   | TacVoid
-  | MetaIdArg      of loc * bool * string
+  | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('constr,'cst,'pat) may_eval
   | IntroPattern   of intro_pattern_expr located
   | Reference      of 'ref
   | Integer        of int
-  | TacCall        of loc *
+  | TacCall        of Loc.t *
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
-  | TacExternal of loc * string * string *
+  | TacExternal of Loc.t * string * string *
       ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
   | TacFreshId     of string or_var list
   | Tacexp of 'tac
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 3223e80b87..568d8a38ec 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Tacexpr
@@ -175,7 +176,7 @@ type module_binder = bool option * lident list * module_ast_inl
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
-  | TacNonTerm of loc * string * (Names.identifier * string) option
+  | TacNonTerm of Loc.t * string * (Names.identifier * string) option
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
@@ -307,7 +308,7 @@ type vernac_expr =
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list list
   | VernacArguments of locality_flag * reference or_by_notation *
-      ((name * bool * (loc * string) option * bool * bool) list) list *
+      ((name * bool * (Loc.t * string) option * bool * bool) list) list *
       int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
   | VernacArgumentsScope of locality_flag * reference or_by_notation *
@@ -355,4 +356,4 @@ type vernac_expr =
   (* For extension *)
   | VernacExtend of string * raw_generic_argument list
 
-and located_vernac_expr = loc * vernac_expr
+and located_vernac_expr = Loc.t * vernac_expr