From 2c0abea33b641b48662c8cd8c2aacc057a66adc1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 9 Apr 2024 21:29:16 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#18909. --- erasure/theories/Typed/Erasure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/erasure/theories/Typed/Erasure.v b/erasure/theories/Typed/Erasure.v index df57eefa6..1ac5ddf0f 100644 --- a/erasure/theories/Typed/Erasure.v +++ b/erasure/theories/Typed/Erasure.v @@ -883,7 +883,7 @@ Solve All Obligations with CoreTactics.equations_simpl; try (reduce_term_sound; destruct r); wfAbstractEnv; eauto with erase. Next Obligation. remember (reduce_term _ _ _ _ _ _) as _b;symmetry in Heq_b. - reduce_term_sound; destruct r; eauto using abstract_env_ext_wf with erase. + reduce_term_sound; destruct r; epose abstract_env_ext_wf; eauto with erase. Qed. Next Obligation. reduce_term_sound.