From df24a81b255190493281ffdeeef36754b076e9cd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 4 Jul 2016 14:36:31 +0200
Subject: Fix reopened bug #3317.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3fbed4b25..214e19fec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -360,7 +360,7 @@ let make_case_or_project env indf ci pred c branches =
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
-     let ctx, br = decompose_lam_assum branch in
+     let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
-- 
cgit v1.2.3