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

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 2410fb7ca..23b9c4d10 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -58,33 +58,33 @@ val jv_nf_betaiotaevar :
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env -> Evd.evar_map -> int * constr * constr ->
+  Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       constr -> constructor -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env -> Evd.evar_map ->
+  Loc.t -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
-  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
@@ -93,10 +93,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
-  env -> Evd.evar_map -> existential_key -> constr -> loc * Evar_kinds.t -> 'b
+  env -> Evd.evar_map -> existential_key -> constr -> Loc.t * Evar_kinds.t -> 'b
 
 val error_unsolvable_implicit :
-  loc -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
+  Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
@@ -115,16 +115,16 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env -> Evd.evar_map -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
-  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env -> Evd.evar_map -> constr -> 'b
+  Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
-val error_var_not_found_loc : loc -> identifier -> 'b
+val error_var_not_found_loc : Loc.t -> identifier -> 'b