From 0ebd3def1fe2bae9c545e8244028197a589cf4db Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 2 Jun 2014 14:46:45 -0400
Subject: Fix check_inductive_codomain.

---
 kernel/inductive.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 192bb69d66..0c80c3a414 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -627,7 +627,9 @@ let branches_specif renv c_spec ci =
 
 let check_inductive_codomain env p =
   let absctx, ar = dest_lam_assum env p in
+  let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
+  let env = push_rel_context arctx env in
   let i,l' = decompose_app (whd_betadeltaiota env s) in
   isInd i
 
-- 
cgit v1.2.3