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, 5 insertions, 5 deletions

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index ea0f063fe4..77985c8d73 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -29,18 +29,18 @@ val new_untyped_evar : unit -> existential_key
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
+  evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> evar_map * constr
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
+  evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+  ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -49,7 +49,7 @@ val new_type_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
@@ -158,7 +158,7 @@ val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
 val split_tycon :
-  loc -> env ->  evar_map -> type_constraint ->
+  Loc.t -> env ->  evar_map -> type_constraint ->
     evar_map * (name * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint