diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3b3c09d384..e1ab02b737 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -895,7 +895,9 @@ let rec find_row_ind = function exception NotCoercible let inh_coerce_to_ind isevars env ty tyi = - let (ntys,_) = splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in + let (ntys,_) = + splay_prod env !isevars + (body_of_type (mis_nf_arity (Global.lookup_mind_specif tyi))) in let (_,evarl) = List.fold_right (fun (na,ty) (env,evl) -> |