Merge pull request #1077 from ppedrot/hint-using-strict-globref

Adapt w.r.t. coq/coq#18909.
MetaCoq · Apr 9, 2024 · eb4ea19 · eb4ea19
2 parents 74918fc + 2c0abea
commit eb4ea19
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.