From 1db7245181073303af78584280ccfa886a56da00 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 31 Aug 2023 15:20:22 +0200 Subject: [PATCH] Adapt to Coq PR #17991 which refolds partially applied fixpoints in simpl. Done by modifying the code so that it is insensitive to the behavior of simpl before and after the Coq PR. --- template-coq/theories/Typing.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v index 30859aa8b..2d398857e 100644 --- a/template-coq/theories/Typing.v +++ b/template-coq/theories/Typing.v @@ -1410,10 +1410,11 @@ Proof. typing_size Hty < S ((typing_spine_size - (fun x (x0 : context) (x1 x2 : term) (x3 : x;;; x0 |- x1 : x2) => - typing_size x3) Σ Γ t_ty l t' t0)) -> + (@typing_size cf) Σ Γ t_ty l t' t0)) -> on_global_env cumul_gen (lift_typing P) Σ.1 * P Σ Γ0 t1 T). { - intros. unshelve eapply X14; eauto. lia. } + intros. unshelve eapply X14; eauto. + change (fun x x0 x1 x2 x3 => typing_size x3) with (@typing_size cf). (* Needed with old versions of "simpl" in "simpl in X14" *) + lia. } clear X14. simpl in pΓ. clear n e H pΓ. induction t0; constructor. unshelve eapply X; clear X; simpl; auto with arith.