Merge pull request #975 from herbelin/master+adapt-coq-pr17991-refold…

…ing-by-simpl-of-fixpoint-partial-application Adapt to coq PR #17991 which lets "simpl" refolds partial applications of fixpoints
MetaCoq · Aug 31, 2023 · 657eb6a · 657eb6a
2 parents 6843d48 + 1db7245
commit 657eb6a
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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.