diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index d81adb6b0..cdf6b523c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -37,47 +37,48 @@ type pretype_error = | VarNotFound of identifier | UnexpectedType of constr * constr | NotProduct of constr + | TypingError of Type_errors.type_error -exception PretypeError of env * pretype_error +exception PretypeError of env * Evd.evar_map * pretype_error val precatchable_exception : exn -> bool (** Presenting terms without solved evars *) -val nf_evar : Evd.evar_map -> constr -> constr -val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment -val jl_nf_evar : - Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list -val jv_nf_evar : - Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array -val tj_nf_evar : - Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment +val nf_evar : Evd.evar_map -> constr -> constr +val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment +val env_nf_evar : Evd.evar_map -> env -> env +val jv_nf_betaiotaevar : + Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array (** Raising errors *) val error_actual_type_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional_loc : - loc -> env -> Evd.evar_map -> + loc -> 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 -> 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 -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_ill_formed_branch_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> constr -> int -> constr -> constr -> 'b val error_number_branches_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> unsafe_judgment -> int -> 'b val error_ill_typed_rec_body_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> int -> name array -> unsafe_judgment array -> types array -> 'b val error_not_a_type_loc : @@ -87,7 +88,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> 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 * Evd.hole_kind -> 'b @@ -112,15 +113,15 @@ 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 -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type_loc : - loc -> env -> Evd.evar_map -> constr -> constr -> 'b + loc -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product_loc : - loc -> env -> Evd.evar_map -> constr -> 'b + loc -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to rawterms } *) |