diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-07-04 14:36:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-06 14:38:05 +0200 |
| commit | df24a81b255190493281ffdeeef36754b076e9cd (patch) | |
| tree | f38db9d81d3646cfab19bded2dea746674fb6e80 /pretyping | |
| parent | f46f4ecec94953930fca6bbbc9fdb83a7a1025fc (diff) | |
Fix reopened bug #3317.
Diffstat (limited to 'pretyping')
| -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 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) -> |