diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3fbed4b252..214e19fecf 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) -> |