From f8295f0d77ab0dd9f989e8e45d43670a69f424df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Mon, 8 Apr 2024 08:27:38 +0200
Subject: [PATCH] Adapt w.r.t. coq/coq#18910.

We guide unification a bit to prevent TC resolution from relying on a previously
transparent Coq primitive.
---
 Theory/Coq/Monad.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Theory/Coq/Monad.v b/Theory/Coq/Monad.v
index 64e2b724..628662b3 100644
--- a/Theory/Coq/Monad.v
+++ b/Theory/Coq/Monad.v
@@ -123,7 +123,7 @@ Open Scope monad_scope.
 Instance Compose_Monad `{Monad M} `{Applicative N}
   `{@Monad_Distributes M N} : Monad (M ∘ N) := {
   ret := λ _ x, ret[M] (pure[N] x);
-  bind := λ _ _ m f, m >>=[M] (mprod M N ∘ ap (pure f));
+  bind := λ x y m f, m >>=[M] (mprod M N ∘ ap (@pure _ _ (x → M (N y)) f));
 }.
 
 #[export]