From 526bc84adb9e892173ad8767bbba38aca4679c8a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 May 2024 11:42:37 +0200 Subject: [PATCH] Fixes for compatibility with Coq master --- erasure-plugin/theories/ErasureCorrectness.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v index b7eeb155a..d5a51f67b 100644 --- a/erasure-plugin/theories/ErasureCorrectness.v +++ b/erasure-plugin/theories/ErasureCorrectness.v @@ -1878,7 +1878,7 @@ Section PCUICErase. now eapply EEtaExpandedFix.expanded_isEtaExp. } specialize (H0 H1). eapply (obseq_lambdabox (Σ', f') (Σ', v'')) in obseq. - epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := lambdabox_pres_app) (Σ', v'') prev H0). + epose proof (ETransformPresAppLam.transform_lam _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0). rewrite -obseq. exact H2. cbn. red; tauto. Qed. @@ -1933,7 +1933,7 @@ Section PCUICErase. now eapply EEtaExpandedFix.expanded_isEtaExp. } specialize (H0 H1). eapply (obseq_lambdabox (Σ', f') (Σ', v'')) in obseq. - epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := lambdabox_pres_app) (Σ', v'') prev H0). + epose proof (ETransformPresAppLam.transform_lam _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0). rewrite -obseq. exact H2. cbn. red; tauto. Qed. @@ -2455,7 +2455,7 @@ Section pipeline_theorem. unshelve eapply (PCUICExpandLetsCorrectness.trans_wcbveval (cf := extraction_checker_flags) (Σ := (Σ.1, Σ.2))). { now eapply PCUICExpandLetsCorrectness.trans_wf. } { clear -HΣ typing''. now eapply PCUICClosedTyp.subject_closed in typing''. } - cbn. 2:cbn. 3:cbn. exact X0. + cbn. 2:cbn. exact X0. now eapply (PCUICExpandLetsCorrectness.trans_axiom_free Σ). pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing''). rewrite PCUICExpandLetsCorrectness.trans_mkApps in X1. eapply X1.