Starting being more explicit on the reasons why module subtyping fails.

Note: I'm unsure about some subtyping error case apparently involving
aliases of inductive types (middle of Subtyping.check_inductive); I
bound it to some NotEqualInductiveAliases error, but this has to be
checked.

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

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c865c92bfb..8252ffb9ed 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -534,15 +534,17 @@ let dest_prod_assum env =
   in
   prodec_rec env empty_rel_context
 
+exception NotArity
+
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match kind_of_term c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> raise NotArity
 
 let is_arity env c =
   try
     let _ = dest_arity env c in
     true
-  with UserError _ -> false
+  with NotArity -> false