diff options
| author | Gaëtan Gilbert | 2019-01-10 14:43:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 5f9a6c17b4353024e7510977a41cfb1de93a0f5f (patch) | |
| tree | 90cad909e39d662f6d7f7293d47c242edd9d4d8e /kernel/type_errors.mli | |
| parent | 05e2222e04323d11429d659b415750cf40e2babd (diff) | |
Move inductive_error to Type_errors
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 3fd40a7f42..613ccb78ca 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -69,6 +69,24 @@ type type_error = (constr, types) ptype_error exception TypeError of env * type_error +(** The different kinds of errors that may result of a malformed inductive + definition. *) +type inductive_error = + | NonPos of env * constr * constr + | NotEnoughArgs of env * constr * constr + | NotConstructor of env * Id.t * constr * constr * int * int + | NonPar of env * constr * int * constr * constr + | SameNamesTypes of Id.t + | SameNamesConstructors of Id.t + | SameNamesOverlap of Id.t list + | NotAnArity of env * constr + | BadEntry + | LargeNonPropInductiveNotInType + +exception InductiveError of inductive_error + +(** Raising functions *) + val error_unbound_rel : env -> int -> 'a val error_unbound_var : env -> variable -> 'a |