diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0f7705317..871f161ab 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -337,6 +337,8 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_glob_constr tomatch) in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in + let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + evdref := evd; let typ = nf_evar !evdref j.uj_type in let t = try try_find_ind env !evdref typ realnames |