Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

1 files changed, 5 insertions, 2 deletions

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 ->