From 8a52cd934118e1064225cffa4248fcb9dd31b898 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Sat, 21 Oct 2023 20:55:38 +0200
Subject: [PATCH] Adapt to Coq/Coq#18164

We want to remove some deprecated Arith files and NPeano from the
stdlib.
---
 tests/Test.v           | 19 ++++++++-----------
 tests/graph.dpd.oracle |  8 ++++----
 tests/search.oracle    |  1 +
 3 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/tests/Test.v b/tests/Test.v
index de3ffa5ef..4e8aeee6f 100644
--- a/tests/Test.v
+++ b/tests/Test.v
@@ -8,7 +8,7 @@
 
 (*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
 
-Require Import Le Gt Minus Min Bool.
+Require Import Arith Bool.
 
 Set Implicit Arguments.
 
@@ -566,7 +566,7 @@ Section Elts.
   Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
   Proof.
     induction l as [|y l].
-    simpl; intros; split; [destruct 1 | apply gt_irrefl].
+    simpl; intros; split; [destruct 1 | apply Nat.lt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
     rewrite Heq; intuition.
     pose (IHl x). intuition.
@@ -695,16 +695,13 @@ Section ListOps.
     simpl (rev (a :: l)).
     simpl (length (a :: l) - S n).
     inversion H.
-    rewrite <- minus_n_n; simpl.
+    rewrite Nat.sub_diag; simpl.
     rewrite <- rev_length.
     rewrite app_nth2; auto.
-    rewrite <- minus_n_n; auto.
-    rewrite app_nth1; auto.
-    rewrite (minus_plus_simpl_l_reverse (length l) n 1).
-    replace (1 + length l) with (S (length l)); auto with arith.
-    rewrite <- minus_Sn_m; [|auto with arith].
-    apply IHl ; auto with arith.
-    rewrite rev_length; auto.
+    rewrite Nat.sub_diag; auto.
+    rewrite app_nth1 by (rewrite rev_length; exact H1).
+    rewrite <-Nat.sub_succ, Nat.sub_succ_l by (exact H1).
+    apply IHl; exact H1.
   Qed.
 
 
@@ -1551,7 +1548,7 @@ Section length_order.
   Proof.
     unfold lel in |- *; intros.
     now_show (length l <= length n).
-    apply le_trans with (length m); auto with arith.
+    apply Nat.le_trans with (length m); auto with arith.
   Qed.
 
   Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
diff --git a/tests/graph.dpd.oracle b/tests/graph.dpd.oracle
index ffbc1519e..15094ae20 100644
--- a/tests/graph.dpd.oracle
+++ b/tests/graph.dpd.oracle
@@ -823,14 +823,14 @@ E: 113 183 [weight=3, ];
 E: 114 181 [weight=1, ];
 E: 114 183 [weight=10, ];
 E: 115 116 [weight=2, ];
-E: 115 121 [weight=36, ];
+E: 115 121 [weight=35, ];
 E: 115 135 [weight=1, ];
 E: 115 136 [weight=1, ];
-E: 115 145 [weight=43, ];
+E: 115 145 [weight=41, ];
 E: 115 169 [weight=10, ];
-E: 115 173 [weight=78, ];
+E: 115 173 [weight=73, ];
 E: 115 179 [weight=1, ];
-E: 115 181 [weight=30, ];
+E: 115 181 [weight=29, ];
 E: 115 182 [weight=37, ];
 E: 115 183 [weight=4, ];
 E: 116 121 [weight=9, ];
diff --git a/tests/search.oracle b/tests/search.oracle
index 605f19805..a2eb1686a 100644
--- a/tests/search.oracle
+++ b/tests/search.oracle
@@ -1,5 +1,6 @@
 Welcome to Coq
 [Loading ML file coq-dpdgraph.plugin ... done]
+[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
 Fetching opaque proofs from disk for dpdgraph.tests.Test
 [cons(42) nil(6) perm_swap(1) perm_skip(3) list(18) Permutation(11) app(43)
 Permutation_trans(3) eq_ind_r(1) eq_ind(2) list_ind(2) Permutation_refl(2)