diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r-- | pretyping/pretype_errors.mli | 74 |
1 files changed, 37 insertions, 37 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index d3e6ffea..3a3dccb4 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,30 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretype_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp open Util open Names open Term open Sign open Environ -open Rawterm +open Glob_term open Inductiveops -(*i*) -(*s The type of errors raised by the pretyper *) +(** {6 The type of errors raised by the pretyper } *) type pretype_error = - (* Old Case *) + (** Old Case *) | CantFindCaseType of constr - (* Unification *) + (** Unification *) | OccurCheck of existential_key * constr | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * @@ -37,51 +33,55 @@ type pretype_error = | CannotFindWellTypedAbstraction of constr * constr list | AbstractionOverMeta of name * name | NonLinearUnification of name * constr - (* Pretyping *) + (** Pretyping *) | 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 +(** 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 env_nf_evar : Evd.evar_map -> env -> env +val env_nf_betaiotaevar : Evd.evar_map -> env -> env +val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment +val jv_nf_betaiotaevar : + Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array -(* Raising errors *) +(** 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 -> - constr -> int -> constr -> constr -> 'b + loc -> env -> Evd.evar_map -> + constr -> constructor -> 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 : @@ -89,9 +89,9 @@ val error_not_a_type_loc : val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b -(*s Implicit arguments synthesis errors *) +(** {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 @@ -113,19 +113,19 @@ val error_abstraction_over_meta : env -> Evd.evar_map -> val error_non_linear_unification : env -> Evd.evar_map -> metavariable -> constr -> 'b -(*s Ml Case errors *) +(** {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 -(*s Pretyping errors *) +(** {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 -(*s Error in conversion from AST to rawterms *) +(** {6 Error in conversion from AST to glob_constr } *) val error_var_not_found_loc : loc -> identifier -> 'b |