From 2e4352419c27446651c8e09a7e27e42d6a5dcd17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Thu, 2 Mar 2023 17:39:52 +0100
Subject: [PATCH] Adapt w.r.t. coq/coq#17322.

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

diff --git a/src/riscv/Platform/MinimalNoMul.v b/src/riscv/Platform/MinimalNoMul.v
index 37d69ff..a646492 100644
--- a/src/riscv/Platform/MinimalNoMul.v
+++ b/src/riscv/Platform/MinimalNoMul.v
@@ -208,8 +208,8 @@ Section Riscv.
       unfold map.getmany_of_tuple, Memory.footprint in IHn.
       specialize IHn with (m := m) (r := (word.add r (word.of_Z 1))).
       rewrite E1 in IHn.
-      specialize IHn with (1 := eq_refl).
       eapply IHn.
+      + reflexivity.
       + instantiate (1 := someSet). clear -H0.
         unfold isXAddr4 in *. fwd. eauto 10 using removeXAddr_bw.
       + unfold Memory.load_bytes in *.