From 70935738326b9044cfb8ef634e78ec67598d7226 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 8 Jan 2026 17:13:21 +0100
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21478

---
 Kami/Ex/IsaRv32.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Kami/Ex/IsaRv32.v b/Kami/Ex/IsaRv32.v
index d832d7f..1e579ee 100644
--- a/Kami/Ex/IsaRv32.v
+++ b/Kami/Ex/IsaRv32.v
@@ -467,7 +467,7 @@ Section RV32IM.
   Definition rv32ToAddr: ToAddrT rv32AddrSize rv32IAddrSize.
     unfold ToAddrT; intros ty iaddr.
     rewrite Haddr3.
-    exact {$0, {#iaddr, $0}}%kami_expr.
+    exact ({$0, {#iaddr, $0}}%kami_expr).
   Defined.
 
   Definition rv32AlignInst: AlignInstT rv32InstBytes rv32DataBytes.