diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 71 |
1 files changed, 41 insertions, 30 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 880f48e5f..c303d5d94 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -9,6 +9,7 @@ open Names open Term open Environ +open EConstr open Type_errors (** {6 The type of errors raised by the pretyper } *) @@ -32,6 +33,8 @@ type position_reporting = (position * int) * constr type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option +type type_error = (constr, types) ptype_error + type pretype_error = (** Old Case *) | CantFindCaseType of constr @@ -64,35 +67,46 @@ exception PretypeError of env * Evd.evar_map * pretype_error val precatchable_exception : exn -> bool (** Raising errors *) -val error_actual_type_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> +val error_actual_type : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> unification_error -> 'b -val error_cant_apply_not_functional_loc : - Loc.t -> env -> Evd.evar_map -> - unsafe_judgment -> unsafe_judgment list -> 'b +val error_actual_type_core : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + +val error_cant_apply_not_functional : + ?loc:Loc.t -> env -> Evd.evar_map -> + unsafe_judgment -> unsafe_judgment array -> 'b -val error_cant_apply_bad_type_loc : - Loc.t -> env -> Evd.evar_map -> int * constr * constr -> - unsafe_judgment -> unsafe_judgment list -> 'b +val error_cant_apply_bad_type : + ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> 'b -val error_case_not_inductive_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b +val error_case_not_inductive : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_ill_formed_branch_loc : - Loc.t -> env -> Evd.evar_map -> +val error_ill_formed_branch : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> pconstructor -> constr -> constr -> 'b -val error_number_branches_loc : - Loc.t -> env -> Evd.evar_map -> +val error_number_branches : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> int -> 'b -val error_ill_typed_rec_body_loc : - Loc.t -> env -> Evd.evar_map -> +val error_ill_typed_rec_body : + ?loc:Loc.t -> env -> Evd.evar_map -> int -> Name.t array -> unsafe_judgment array -> types array -> 'b -val error_not_a_type_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b +val error_elim_arity : + ?loc:Loc.t -> env -> Evd.evar_map -> + pinductive -> sorts_family list -> constr -> + unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + +val error_not_a_type : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + +val error_assumption : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b @@ -101,15 +115,12 @@ 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_unsolvable_implicit : - Loc.t -> env -> Evd.evar_map -> existential_key -> + ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b -val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map -> +val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> ?reason:unification_error -> constr * constr -> 'b -val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error -> - constr * constr -> 'b - val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> @@ -126,20 +137,20 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) -val error_cant_find_case_type_loc : - Loc.t -> env -> Evd.evar_map -> constr -> 'b +val error_cant_find_case_type : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) -val error_unexpected_type_loc : - Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b +val error_unexpected_type : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b -val error_not_product_loc : - Loc.t -> env -> Evd.evar_map -> constr -> 'b +val error_not_product : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) -val error_var_not_found_loc : Loc.t -> Id.t -> 'b +val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b (** {6 Typeclass errors } *) |