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

1 files changed, 6 insertions, 2 deletions

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