Commit 6a295a21 authored by Robbert Krebbers's avatar Robbert Krebbers

Comment about coercion.

parent 45b9c079
......@@ -708,6 +708,8 @@ Class oFunctorContractive (F : oFunctor) :=
Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
Hint Mode oFunctorContractive ! : typeclass_instances.
(** Not a coercion due to the [Cofe] type class argument, and to avoid
ambiguous coercion paths, see *)
Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
oFunctor_car F A A.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment