diff options
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b4c3a2bbda..f539d3685f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -972,7 +972,7 @@ let case_dependent env sigma loc predj tomatchs = in let etapred = eta_expand env sigma predj.uj_val (body_of_type predj.uj_type) in let n = nb_lam etapred in - let _,sort = decomp_prod env sigma (body_of_type predj.uj_type) in + let _,sort = splay_prod env sigma (body_of_type predj.uj_type) in let ndepv = List.map nb_dep_ity tomatchs in let sum = List.fold_right (fun i j -> i+j) ndepv 0 in let depsum = sum + List.length tomatchs in |