From 082b9f2efb4a775caa2b49dafc1dfcfd09cf9948 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Wed, 15 Jan 2014 18:51:36 -0500
Subject: Christmas is over...

---
 checker/inductive.ml |  7 ++++---
 kernel/inductive.ml  | 24 ++++++++++++------------
 2 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index ad7c472d9..be0f220b2 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -281,9 +281,10 @@ let is_correct_arity env c (p,pj) ind specif params =
           (try conv env a1 a1'
           with NotConvertible -> raise (LocalArity None));
           srec (push_rel (na1,None,a1) env) t ar'
-      | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
-          let ksort = match (whd_betadeltaiota env a2) with
-            | Sort s -> family_of_sort s
+      | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
+	 let env' = push_rel (na1,None,a1) env in
+     let ksort = match (whd_betadeltaiota env' a2) with
+        | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
 	  let dep_ind = build_dependent_inductive ind specif params in
           (try conv env a1 dep_ind
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fca72e3ae..5c1006438 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -304,18 +304,18 @@ let is_correct_arity env c pj ind specif params =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
           srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ)
-      | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
-          let ksort = match kind_of_term (whd_betadeltaiota env a2) with
-            | Sort s -> family_of_sort s
-	    | _ -> raise (LocalArity None) in
-	  let dep_ind = build_dependent_inductive ind specif params in
-          let univ =
-            try conv env a1 dep_ind
-            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
+      (* The last Prod domain is the type of the scrutinee *)
+      | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
+	 let env' = push_rel (na1,None,a1) env in
+	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
+       | Sort s -> family_of_sort s
+       | _ -> raise (LocalArity None) in
+	 let dep_ind = build_dependent_inductive ind specif params in
+	 let univ =
+           try conv env a1 dep_ind
+           with NotConvertible -> raise (LocalArity None) in
+	 check_allowed_sort ksort specif;
+	 union_constraints u univ
       | _ ->
 	  raise (LocalArity None)
   in
-- 
cgit v1.2.3