From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- kernel/indtypes.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0dd2cd69..9ca838fc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -42,7 +42,7 @@ type inductive_error = | SameNamesTypes of identifier | SameNamesConstructors of identifier | SameNamesOverlap of identifier list - | NotAnArity of identifier + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType @@ -254,7 +254,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 -> -- cgit v1.2.3