From 964dc89064da3232ffb202474bf9b775c581ee5c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 3 May 2023 15:30:52 +0200
Subject: [PATCH] Adapt w.r.t. coq/coq#17564.

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

diff --git a/src/Loops.v b/src/Loops.v
index ab17db3..c080dc7 100644
--- a/src/Loops.v
+++ b/src/Loops.v
@@ -271,7 +271,7 @@ Module Import core.
             try (rewrite loop_fuel_0 in Hs; congruence); [].
           pose proof (iterations_required_step _ _ s' _ Hs' Hstep) as HA.
           rewrite HA.
-          destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]].
+          edestruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]].
           pose proof (HE' ltac:(constructor)) as HE; clear HE'.
           split; [|lia].
           rewrite loop_fuel_S_first, Hstep in Hs.