From 2a5aee8a94855c4457a4b456bebe399d24bcd1e5 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Wed, 1 Nov 2023 10:30:55 +0100 Subject: [PATCH] Adapt to Coq/Coq#18164 --- src/FrapTactics.v | 8 ++++---- src/Minimalistic.v | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/FrapTactics.v b/src/FrapTactics.v index dc0b425..0801e3c 100644 --- a/src/FrapTactics.v +++ b/src/FrapTactics.v @@ -51,16 +51,16 @@ Ltac propositional := intuition idtac. Ltac linear_arithmetic := intros; repeat match goal with | [ |- context[max ?a ?b] ] => - let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]]; + let Heq := fresh "Heq" in destruct (Nat.max_spec a b) as [[? Heq] | [? Heq]]; rewrite Heq in *; clear Heq | [ _ : context[max ?a ?b] |- _ ] => - let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]]; + let Heq := fresh "Heq" in destruct (Nat.max_spec a b) as [[? Heq] | [? Heq]]; rewrite Heq in *; clear Heq | [ |- context[min ?a ?b] ] => - let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]]; + let Heq := fresh "Heq" in destruct (Nat.min_spec a b) as [[? Heq] | [? Heq]]; rewrite Heq in *; clear Heq | [ _ : context[min ?a ?b] |- _ ] => - let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]]; + let Heq := fresh "Heq" in destruct (Nat.min_spec a b) as [[? Heq] | [? Heq]]; rewrite Heq in *; clear Heq end; lia. diff --git a/src/Minimalistic.v b/src/Minimalistic.v index 20f2649..9354c76 100644 --- a/src/Minimalistic.v +++ b/src/Minimalistic.v @@ -2314,7 +2314,7 @@ Section Language. Lemma old_different i n x : index_old n i -> i <> pos_pair (S n, x). Proof. - intros ??; subst; eauto using pos_pair_old_conv, gt_Sn_n. + intros ??; subst; eauto using pos_pair_old_conv, Nat.lt_succ_diag_r. Qed. Lemma pos_pair_inj_left n m x y : pos_pair (n, x) = pos_pair (m, y) ->