diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5a99adb5a..a8af39bc7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -129,7 +129,7 @@ module Default = struct match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> - let (evd',t) = define_evar_as_arrow evd ev in + let (evd',t) = define_evar_as_product evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try |