Adapt w.r.t. coq/coq#17564.

mit-plv · May 4, 2023 · 1cce238 · 1cce238
1 parent 79642ca
commit 1cce238
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Util/Loops.v b/src/Util/Loops.v
@@ -270,7 +270,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.