aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-04 14:36:31 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-07-06 14:38:05 +0200
commitdf24a81b255190493281ffdeeef36754b076e9cd (patch)
treef38db9d81d3646cfab19bded2dea746674fb6e80 /pretyping
parentf46f4ecec94953930fca6bbbc9fdb83a7a1025fc (diff)
Fix reopened bug #3317.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/inductiveops.ml2
1 files changed, 1 insertions, 1 deletions
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) ->