From efc3f81ba61135cf86dcdb15fd3469b412fc1ff0 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 2 Apr 2026 11:16:58 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21849

---
 src/WithItreeWIP.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/WithItreeWIP.v b/src/WithItreeWIP.v
index f52caaf..089599d 100644
--- a/src/WithItreeWIP.v
+++ b/src/WithItreeWIP.v
@@ -12,7 +12,7 @@ Module interaction.
   | interact {R : Type} (e : E R) (k : R -> interaction)
   | ret (_ : T).
   Arguments interaction : clear implicits.
-  Arguments interaction _%eff _%type.
+  Arguments interaction _%_eff _%_type.
 
   Section bind.
     Context {E : Type -> Type} {T U : Type} (k : T -> interaction E U).