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

---
 checker/inductive.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'checker')

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
-- 
cgit v1.2.3