Fixing #2846: Uncaught exception Reduction.NotArity.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7

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