Christmas is over...

1 files changed, 12 insertions, 12 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fca72e3aee..5c10064385 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