Relaxing the sort elimination check to allow for let-bindings in arities.

I restored this in the kernel, and added it to the checker. There is one last
source of non-uniformity, which is the Sort case in the checker (was not
present in the kernel). I don't know what this case covers, so it should be
reviewed.

1 files changed, 2 insertions, 0 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5c10064385..abc6ba4dfb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -316,6 +316,8 @@ let is_correct_arity env c pj ind specif params =
            with NotConvertible -> raise (LocalArity None) in
 	 check_allowed_sort ksort specif;
 	 union_constraints u univ
+      | _, (_,Some _,_ as d)::ar' ->
+	 srec (push_rel d env) (lift 1 pt') ar' u
       | _ ->
 	  raise (LocalArity None)
   in