From c15c10908f764c7b1016f699160bfaba4e7e848a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 23 Aug 2013 15:40:57 +0000
Subject: Fix computation of discharged hyps for inductive types forgetting the
 conclusion of the arity.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16732 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a695372314..9a11e47dc3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -598,8 +598,12 @@ let allowed_sorts issmall isunit s =
   | InProp -> logical_sorts
 
 let fold_inductive_blocks f =
-  Array.fold_left (fun acc (_,_,lc,(arsign,_)) ->
-    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign))
+  let concl = function
+    | Inr _ -> mkSet (* dummy *)
+    | Inl (_,ar,_) -> ar
+  in
+    Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
+      f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (concl ar) arsign))
 
 let used_section_variables env inds =
   let ids = fold_inductive_blocks
-- 
cgit v1.2.3