diff options
-rw-r--r-- | kernel/indtypes.ml | 7 | ||||
-rw-r--r-- | kernel/indtypes.mli | 2 | ||||
-rw-r--r-- | toplevel/himsg.ml | 6 |
3 files changed, 9 insertions, 6 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e0bfb69ae..a69537231 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -45,7 +45,7 @@ type inductive_error = | SameNamesTypes of Id.t | SameNamesConstructors of Id.t | SameNamesOverlap of Id.t list - | NotAnArity of Id.t + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType @@ -262,7 +262,10 @@ let typecheck_inductive env mie = let ind_min_levels = inductive_levels arities inds in let inds, cst = Array.fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> - let sign, s = dest_arity env full_arity in + let sign, s = + try dest_arity env full_arity + with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) + in let status,cst = match s with | Type u when ar_level != None (* Explicitly polymorphic *) && no_upper_constraints u cst -> diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 0d3d1bdff..ce789b00e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -28,7 +28,7 @@ type inductive_error = | SameNamesTypes of Id.t | SameNamesConstructors of Id.t | SameNamesOverlap of Id.t list - | NotAnArity of Id.t + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 616dfb941..6f7696fab 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -908,8 +908,8 @@ let error_same_names_overlap idl = str "names:" ++ spc () ++ prlist_with_sep pr_comma pr_id idl ++ str "." -let error_not_an_arity id = - str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." +let error_not_an_arity env c = + str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "is not an arity." let error_bad_entry () = str "Bad inductive definition." @@ -945,7 +945,7 @@ let explain_inductive_error = function | SameNamesTypes id -> error_same_names_types id | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl - | NotAnArity id -> error_not_an_arity id + | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () |