diff options
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 11729171b..c342ce892 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -9,7 +9,6 @@ (*i $Id$ i*) (*i*) -open Pp open Names open Term open Sign @@ -41,62 +40,63 @@ type guard_error = type type_error = | UnboundRel of int | NotAType of unsafe_judgment - | BadAssumption of constr - | ReferenceVariables of identifier + | BadAssumption of unsafe_judgment + | ReferenceVariables of constr | ElimArity of inductive * constr list * constr * unsafe_judgment * (constr * constr * string) option | CaseNotInductive of unsafe_judgment + | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * int * constr * constr | Generalization of (name * types) * unsafe_judgment - | ActualType of constr * constr * constr + | ActualType of unsafe_judgment * types | CantApplyBadType of (int * constr * constr) - * unsafe_judgment * unsafe_judgment list - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list + * unsafe_judgment * unsafe_judgment array + | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array | IllFormedRecBody of guard_error * name array * int * constr array | IllTypedRecBody of int * name array * unsafe_judgment array * types array -exception TypeError of path_kind * env * type_error +exception TypeError of env * type_error -val error_unbound_rel : path_kind -> env -> int -> 'a +val error_unbound_rel : env -> int -> 'a -val error_not_type : path_kind -> env -> unsafe_judgment -> 'a +val error_not_type : env -> unsafe_judgment -> 'a -val error_assumption : path_kind -> env -> constr -> 'a +val error_assumption : env -> unsafe_judgment -> 'a -val error_reference_variables : path_kind -> env -> identifier -> 'a +val error_reference_variables : env -> constr -> 'a val error_elim_arity : - path_kind -> env -> inductive -> constr list -> constr + env -> inductive -> constr list -> constr -> unsafe_judgment -> (constr * constr * string) option -> 'a val error_case_not_inductive : - path_kind -> env -> unsafe_judgment -> 'a + env -> unsafe_judgment -> 'a val error_number_branches : - path_kind -> env -> unsafe_judgment -> int -> 'a + env -> unsafe_judgment -> int -> 'a val error_ill_formed_branch : - path_kind -> env -> constr -> int -> constr -> constr -> 'a + env -> constr -> int -> constr -> constr -> 'a val error_generalization : - path_kind -> env -> name * types -> unsafe_judgment -> 'a + env -> name * types -> unsafe_judgment -> 'a val error_actual_type : - path_kind -> env -> constr -> constr -> constr -> 'a + env -> unsafe_judgment -> types -> 'a val error_cant_apply_not_functional : - path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'a + env -> unsafe_judgment -> unsafe_judgment array -> 'a val error_cant_apply_bad_type : - path_kind -> env -> int * constr * constr -> - unsafe_judgment -> unsafe_judgment list -> 'a + env -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - path_kind -> env -> guard_error -> name array -> int -> constr array -> 'a + env -> guard_error -> name array -> int -> constr array -> 'a val error_ill_typed_rec_body : - path_kind -> env -> int -> name array -> unsafe_judgment array + env -> int -> name array -> unsafe_judgment array -> types array -> 'a |