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 04cb6a59f..6dc3687a0 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -251,7 +251,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let (n, dom, rng) = destLambda !evdref t in if isEvar !evdref dom then let (domk, args) = destEvar !evdref dom in - evdref := define domk (EConstr.Unsafe.to_constr a) !evdref; + evdref := define domk a !evdref; else (); t, rng | _ -> raise NoSubtacCoercion |