Christmas is over...

1 files changed, 4 insertions, 3 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index ad7c472d99..be0f220b28 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