From 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sat, 18 Jan 2014 15:09:40 -0500
Subject: 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.
---
 checker/inductive.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index be0f220b2..c00a6c5dd 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -294,6 +294,8 @@ let is_correct_arity env c (p,pj) ind specif params =
       | Sort s', [] ->
 	  check_allowed_sort (family_of_sort s') specif;
 	  false
+      | _, (_,Some _,_ as d)::ar' ->
+	 srec (push_rel d env) (lift 1 pt') ar' u
       | _ ->
 	  raise (LocalArity None)
   in
-- 
cgit v1.2.3