Adapt to coq/coq#18164

mit-plv · Nov 6, 2023 · 2a5aee8 · 2a5aee8
1 parent 964dc89
commit 2a5aee8
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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) ->