diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 28 |
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 |