diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r-- | pretyping/pretype_errors.mli | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli new file mode 100644 index 00000000..ebeff99d --- /dev/null +++ b/pretyping/pretype_errors.mli @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: pretype_errors.mli,v 1.25.2.3 2004/07/16 19:30:45 herbelin Exp $ i*) + +(*i*) +open Pp +open Util +open Names +open Term +open Sign +open Environ +open Rawterm +open Inductiveops +(*i*) + +(*s The type of errors raised by the pretyper *) + +type pretype_error = + (* Old Case *) + | CantFindCaseType of constr + (* Unification *) + | OccurCheck of existential_key * constr + | NotClean of existential_key * constr * hole_kind + | UnsolvableImplicit of hole_kind + (* Pretyping *) + | VarNotFound of identifier + | UnexpectedType of constr * constr + | NotProduct of constr + +exception PretypeError of env * pretype_error + +(* 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 + + +(* Raising errors *) +val error_actual_type_loc : + loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + +val error_cant_apply_not_functional_loc : + 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 -> + unsafe_judgment -> unsafe_judgment list -> 'b + +val error_case_not_inductive_loc : + loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b + +val error_ill_formed_branch_loc : + loc -> env -> Evd.evar_map -> + constr -> int -> constr -> constr -> 'b + +val error_number_branches_loc : + loc -> env -> Evd.evar_map -> + unsafe_judgment -> int -> 'b + +val error_ill_typed_rec_body_loc : + loc -> env -> Evd.evar_map -> + int -> name array -> unsafe_judgment array -> types array -> 'b + +(*s Implicit arguments synthesis errors *) + +val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b + +val error_not_clean : + env -> Evd.evar_map -> existential_key -> constr -> loc * hole_kind -> 'b + +val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b + +(*s Ml Case errors *) + +val error_cant_find_case_type_loc : + loc -> env -> Evd.evar_map -> constr -> 'b + +(*s Pretyping errors *) + +val error_unexpected_type_loc : + loc -> env -> Evd.evar_map -> constr -> constr -> 'b + +val error_not_product_loc : + loc -> env -> Evd.evar_map -> constr -> 'b + +(*s Error in conversion from AST to rawterms *) + +val error_var_not_found_loc : loc -> identifier -> 'b |