From e7f13672e04d732e19fd44b4cfc45abf4bf5bd51 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 1 Apr 2026 11:36:34 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21851

---
 test-suite/bug3.v             | 7 +++----
 test-suite/bug4.v             | 4 +---
 test-suite/bug5.v             | 5 ++---
 test-suite/exmNotParametric.v | 2 +-
 test-suite/features.v         | 4 ++--
 test-suite/wadler.v           | 3 +--
 6 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/test-suite/bug3.v b/test-suite/bug3.v
index 9ca7ac0..20498a4 100644
--- a/test-suite/bug3.v
+++ b/test-suite/bug3.v
@@ -1,9 +1,8 @@
 Declare ML Module "coq-paramcoq.plugin".
 
-Require Import PeanoNat.
-Require Import Recdef.
+From Stdlib Require Import PeanoNat Recdef.
 Set Implicit Arguments.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Fixpoint subS (n m : nat) {struct n} : nat :=
   match n return  nat with
@@ -90,7 +89,7 @@ Global Parametricity Tactic := ((destruct_reflexivity; fail)
                             || (destruct_reflexivity_with_nat_arg_pattern; fail)
                             ||  auto). 
 
-Require Import ProofIrrelevance.
+From Stdlib Require Import ProofIrrelevance.
 
 (* Parametricity Recursive GcdS qualified. *)  (* FIXME *)
 
diff --git a/test-suite/bug4.v b/test-suite/bug4.v
index 9f1ba9d..b3ecc3b 100644
--- a/test-suite/bug4.v
+++ b/test-suite/bug4.v
@@ -1,8 +1,6 @@
-
 Declare ML Module "coq-paramcoq.plugin".
 
-Require Import PeanoNat.
-Require Import PArith.
+From Stdlib Require Import PeanoNat PArith.
 
 Print BinPosDef.Pos.sub_mask.
 
diff --git a/test-suite/bug5.v b/test-suite/bug5.v
index bad155f..92b86d9 100644
--- a/test-suite/bug5.v
+++ b/test-suite/bug5.v
@@ -1,7 +1,6 @@
 Declare ML Module "coq-paramcoq.plugin".
 
-Require Import PeanoNat.
-Require Import Recdef.
+From Stdlib Require Import PeanoNat Recdef.
 Set Implicit Arguments.
 
 
@@ -76,7 +75,7 @@ Proof.
 Defined.
 
 
-Require Import ProofIrrelevance.
+From Stdlib Require Import ProofIrrelevance.
 Parametricity Recursive sig_rec.
 
 Ltac destruct_reflexivity := 
diff --git a/test-suite/exmNotParametric.v b/test-suite/exmNotParametric.v
index bf63aae..0e272c8 100644
--- a/test-suite/exmNotParametric.v
+++ b/test-suite/exmNotParametric.v
@@ -1,4 +1,4 @@
-From Coq Require Import ClassicalFacts.
+From Stdlib Require Import ClassicalFacts.
 Inductive False_R : False -> False -> Prop :=.
 
 Inductive or_R (A₁ A₂ : Prop) (A_R : A₁ -> A₂ -> Prop) (B₁ B₂ : Prop)
diff --git a/test-suite/features.v b/test-suite/features.v
index 081f055..83d4d35 100644
--- a/test-suite/features.v
+++ b/test-suite/features.v
@@ -3,7 +3,7 @@ Require Import Parametricity.
 
 (** Separate compilation: *)
 Parametricity nat as test.
-Require List.
+From Stdlib Require List.
 
 Parametricity Recursive List.rev.
 Check rev_R.
@@ -51,7 +51,7 @@ End Test.
 
 (** Opaque terms. **)
 
-Require ProofIrrelevance.
+From Stdlib Require ProofIrrelevance.
 
 Lemma opaque : True.
 trivial.
diff --git a/test-suite/wadler.v b/test-suite/wadler.v
index 0235fbf..21e2a78 100644
--- a/test-suite/wadler.v
+++ b/test-suite/wadler.v
@@ -1,5 +1,4 @@
-
-Require Import List.
+From Stdlib Require Import List.
 Require Import Parametricity.
 
 Lemma nat_R_equal :