From 6a295a21d60ea1a9bf6d469df2012b47a5122763 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:29:34 +0200
Subject: [PATCH] Comment about coercion.
---
theories/algebra/ofe.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index e7197b7df..07b2993a1 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -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 https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
oFunctor_car F A A.
--
GitLab