From 37e6aa6e206b75a151dc2cc939a60d66b2691e2b Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 31 Mar 2026 17:06:20 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21851

---
 src/reify.ml                                |  2 +-
 theories/BoolView.v                         |  5 ++---
 theories/ChurchRosser_Points_vs_Algebraic.v |  2 +-
 theories/Common.v                           | 10 +++++-----
 theories/DKA_Construction.v                 |  2 +-
 theories/DKA_DFA_Equiv.v                    |  4 ++--
 theories/DKA_DFA_Language.v                 |  3 +--
 theories/DKA_Definitions.v                  |  2 +-
 theories/DKA_Epsilon.v                      |  4 ++--
 theories/DecideKleeneAlgebra.v              |  2 +-
 theories/Examples.v                         |  2 +-
 theories/Force.v                            |  4 ++--
 theories/Model_Languages.v                  |  3 +--
 theories/Model_Relations.v                  |  1 -
 theories/Model_StdRelations.v               |  2 +-
 theories/MxGraph.v                          |  2 +-
 theories/MyFMapProperties.v                 |  2 +-
 theories/MyFSetProperties.v                 |  3 +--
 theories/MyFSets.v                          |  7 +++----
 theories/Numbers.v                          |  3 +--
 theories/Reification.v                      |  4 ++--
 theories/SemiRing.v                         |  1 -
 theories/StrictStarForm.v                   |  2 +-
 theories/Utils_WF.v                         |  2 +-
 24 files changed, 33 insertions(+), 41 deletions(-)

diff --git a/src/reify.ml b/src/reify.ml
index 0ebd202..72dce5b 100644
--- a/src/reify.ml
+++ b/src/reify.ml
@@ -51,7 +51,7 @@ let get_fun_5 d s = let v = get_const d s in fun x y z t u -> force_app v [|x;y;
 (* Coq constants *)
 module Coq = struct
   (* binary positive numbers *)
-  let positive_path = ["Coq" ; "Numbers"; "BinNums"]
+  let positive_path = ["Corelib" ; "Numbers"; "BinNums"]
   let positive = get_const positive_path "positive"
   let xH = get_const positive_path "xH"
   let xI = get_fun_1 positive_path "xI"
diff --git a/theories/BoolView.v b/theories/BoolView.v
index 3cf222e..ce8ffd2 100644
--- a/theories/BoolView.v
+++ b/theories/BoolView.v
@@ -31,8 +31,8 @@
 *)
 
 From ATBR Require Import Common.
-From Coq Require Export Bool.
-From Coq Require Import Equality Program Sumbool Peano.
+From Stdlib Require Export Bool.
+From Stdlib Require Import Equality Program Sumbool Peano.
 
 #[local] Ltac Tauto.intuition_solver ::= auto with exfalso lia.
 
@@ -256,4 +256,3 @@ Ltac completer tac:=
     | [H : ?x = ?y |- _ ]  => subst H
     | _ => tac
   end.
-
diff --git a/theories/ChurchRosser_Points_vs_Algebraic.v b/theories/ChurchRosser_Points_vs_Algebraic.v
index 66c1729..2c83f04 100644
--- a/theories/ChurchRosser_Points_vs_Algebraic.v
+++ b/theories/ChurchRosser_Points_vs_Algebraic.v
@@ -12,7 +12,7 @@
     href="ChurchRosser_Points_vs_Algebraic.v">here</a>#. *)
 
 From ATBR Require Import ATBR.
-From Coq Require Import Relations.
+From Stdlib Require Import Relations.
 
 (** * Standard proof: binary relations relate points to points *)
 Section CR_points.
diff --git a/theories/Common.v b/theories/Common.v
index ce5d286..1f07553 100644
--- a/theories/Common.v
+++ b/theories/Common.v
@@ -9,11 +9,11 @@
 (** This small module is imported in all our files, it exports useful
    modules and defines some basic utilities and tactics *)
 
-From Coq Require Export Arith.
-From Coq Require Export Lia.
-From Coq Require Export BinNums BinPos PArith.Pnat.
-From Coq Require Export Program.Equality. 
-From Coq Require Export Setoid Morphisms. 
+From Stdlib Require Export Arith.
+From Stdlib Require Export Lia.
+From Stdlib Require Export BinNums BinPos PArith.Pnat.
+From Stdlib Require Export Program.Equality. 
+From Stdlib Require Export Setoid Morphisms. 
 
 Set Implicit Arguments.
 
diff --git a/theories/DKA_Construction.v b/theories/DKA_Construction.v
index b46e17e..9af14c5 100644
--- a/theories/DKA_Construction.v
+++ b/theories/DKA_Construction.v
@@ -34,7 +34,7 @@ From ATBR Require Import DKA_CheckLabels.
 From ATBR Require Import StrictStarForm.
 
 From ATBR Require Import Utils_WF.
-From Coq Require Import Relations.
+From Stdlib Require Import Relations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/DKA_DFA_Equiv.v b/theories/DKA_DFA_Equiv.v
index 00ce60c..9fad609 100644
--- a/theories/DKA_DFA_Equiv.v
+++ b/theories/DKA_DFA_Equiv.v
@@ -25,8 +25,8 @@ From ATBR Require Import DKA_StateSetSets.
 From ATBR Require DKA_DFA_Language.
 
 From ATBR Require Import Utils_WF.
-From Coq Require Import Relations.
-From Coq Require Import List.
+From Stdlib Require Import Relations.
+From Stdlib Require Import List.
 
 Import DSUtils.Notations.
 
diff --git a/theories/DKA_DFA_Language.v b/theories/DKA_DFA_Language.v
index 2503cc2..ffda8ef 100644
--- a/theories/DKA_DFA_Language.v
+++ b/theories/DKA_DFA_Language.v
@@ -13,7 +13,7 @@
    procedure.
    *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 
 From ATBR Require Import Common.
 From ATBR Require Import Classes.
@@ -276,4 +276,3 @@ Proof.
 Qed.
 
 End protect.
-
diff --git a/theories/DKA_Definitions.v b/theories/DKA_Definitions.v
index 901ebdc..9864083 100644
--- a/theories/DKA_Definitions.v
+++ b/theories/DKA_Definitions.v
@@ -32,7 +32,7 @@ Export RegExp.Load.
 From ATBR Require Import MyFSets.
 From ATBR Require Import MyFSetProperties.
 From ATBR Require Import MyFMapProperties.
-From Coq Require FMapAVL.
+From Stdlib Require FMapAVL.
 From ATBR Require Numbers.
 Export Numbers.PositiveUtils.
 
diff --git a/theories/DKA_Epsilon.v b/theories/DKA_Epsilon.v
index 36fe12b..5c24612 100644
--- a/theories/DKA_Epsilon.v
+++ b/theories/DKA_Epsilon.v
@@ -24,8 +24,8 @@ From ATBR Require Import MxKleeneAlgebra.
 From ATBR Require Import DKA_Definitions.
 
 From ATBR Require Import Utils_WF.
-From Coq Require Import Relations.
-From Coq Require Import Eqdep_dec.
+From Stdlib Require Import Relations.
+From Stdlib Require Import Eqdep_dec.
 
 
 Set Implicit Arguments.
diff --git a/theories/DecideKleeneAlgebra.v b/theories/DecideKleeneAlgebra.v
index b28881b..11d6543 100644
--- a/theories/DecideKleeneAlgebra.v
+++ b/theories/DecideKleeneAlgebra.v
@@ -24,7 +24,7 @@ From ATBR Require DKA_DFA_Equiv.
 From ATBR Require StrictStarForm.
 From ATBR Require Reification.
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 
 Definition word := list positive.
 Inductive CounterExample: Set :=
diff --git a/theories/Examples.v b/theories/Examples.v
index 88dcfba..bafb235 100644
--- a/theories/Examples.v
+++ b/theories/Examples.v
@@ -319,7 +319,7 @@ End Concrete.
     declared in Model_StdRelations, so that one can use our tactics to
     reason about these.  *)
 
-From Coq Require Relations.
+From Stdlib Require Relations.
 From ATBR Require Model_StdRelations.
 
 Section Concrete'.
diff --git a/theories/Force.v b/theories/Force.v
index 9dad6ee..36a4d7f 100644
--- a/theories/Force.v
+++ b/theories/Force.v
@@ -9,8 +9,8 @@
 (** Memoisation function for matrices: we define an identity function
    that enforces evaluation *)
 
-From Coq Require Import List.
-From Coq Require Import Arith.
+From Stdlib Require Import List.
+From Stdlib Require Import Arith.
 
 Set Implicit Arguments.
 
diff --git a/theories/Model_Languages.v b/theories/Model_Languages.v
index 38bcc59..ded57ed 100644
--- a/theories/Model_Languages.v
+++ b/theories/Model_Languages.v
@@ -12,7 +12,7 @@ From ATBR Require Import Common.
 From ATBR Require Import Classes.
 From ATBR Require Import MxGraph.
 From ATBR Require Converse.
-From Coq Require Import List.
+From Stdlib Require Import List.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -170,4 +170,3 @@ Module Load.
               change (@lang_star A) with (@star (@lang_Graph A) (@lang_Star_Op A) tt).
     
 End Load.
-
diff --git a/theories/Model_Relations.v b/theories/Model_Relations.v
index b007f08..0b6c2b3 100644
--- a/theories/Model_Relations.v
+++ b/theories/Model_Relations.v
@@ -146,4 +146,3 @@ Module Load.
               change rel_star with (@star rel_Graph rel_Star_Op).
     
 End Load.
-
diff --git a/theories/Model_StdRelations.v b/theories/Model_StdRelations.v
index f235935..d4c67be 100644
--- a/theories/Model_StdRelations.v
+++ b/theories/Model_StdRelations.v
@@ -11,7 +11,7 @@
 From ATBR Require Import Common.
 From ATBR Require Import Classes.
 From ATBR Require Converse.
-From Coq Require Import Relations.
+From Stdlib Require Import Relations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/MxGraph.v b/theories/MxGraph.v
index 610aa05..0b64f0a 100644
--- a/theories/MxGraph.v
+++ b/theories/MxGraph.v
@@ -11,7 +11,7 @@
 From ATBR Require Import Common.
 From ATBR Require Import Classes.
 From ATBR Require Import Graph.
-From Coq Require List.
+From Stdlib Require List.
 From ATBR Require Force.
 
 Set Implicit Arguments.
diff --git a/theories/MyFMapProperties.v b/theories/MyFMapProperties.v
index 7b78b67..c5ef1cc 100644
--- a/theories/MyFMapProperties.v
+++ b/theories/MyFMapProperties.v
@@ -8,7 +8,7 @@
 
 (** Handler for FMap properties, provides the [find_tac] tactic. *)
 
-From Coq Require Import FMaps.
+From Stdlib Require Import FMaps.
 From ATBR Require Import Common.
 From ATBR Require Import BoolView.
 
diff --git a/theories/MyFSetProperties.v b/theories/MyFSetProperties.v
index 1fa883c..395f64c 100644
--- a/theories/MyFSetProperties.v
+++ b/theories/MyFSetProperties.v
@@ -38,7 +38,7 @@
    acc) m]), one will use [set_induction_below] and rewrite the lemma
    [fold_add_below] *)
 
-From Coq Require Import FSets.
+From Stdlib Require Import FSets.
 From ATBR Require Import Common.
 From ATBR Require Import BoolView.
 
@@ -367,4 +367,3 @@ Module MySetProps (X : FSetInterface.S).
   Qed.
 
 End MySetProps.  
-
diff --git a/theories/MyFSets.v b/theories/MyFSets.v
index 742dd01..6f472cf 100644
--- a/theories/MyFSets.v
+++ b/theories/MyFSets.v
@@ -12,9 +12,9 @@
    TODO: Coq standard library has evolved in v8.3, so that (parts of)
    this file might no longer be useful.  *)
 
-From Coq Require Export FMaps FSets.
-From Coq Require Import List.
-From Coq Require Import NArith.
+From Stdlib Require Export FMaps FSets.
+From Stdlib Require Import List.
+From Stdlib Require Import NArith.
 
 (** Functors to perform "transparent sealing". *)
 Module FSetHide (X : FSetInterface.S).
@@ -233,4 +233,3 @@ End PairOrderedType.
 
 Module Nat_as_OT := OrderedType_from_Alt Nat_as_OTA.
 Module Pos_as_OT := OrderedType_from_Alt Pos_as_OTA.
-
diff --git a/theories/Numbers.v b/theories/Numbers.v
index d8df89d..9c5c932 100644
--- a/theories/Numbers.v
+++ b/theories/Numbers.v
@@ -28,7 +28,7 @@
 From ATBR Require Import Common.
 From ATBR Require Import BoolView.
 From ATBR Require Import MyFSets MyFSetProperties MyFMapProperties.
-From Coq Require Import FSetPositive FMapPositive.
+From Stdlib Require Import FSetPositive FMapPositive.
 
 #[local] Ltac Tauto.intuition_solver ::= auto with bool lia.
 
@@ -517,4 +517,3 @@ Module Positive <: NUM.
 End Positive.
 
 Module PositiveUtils := NumUtils Positive.
-
diff --git a/theories/Reification.v b/theories/Reification.v
index 10a4962..62297c5 100644
--- a/theories/Reification.v
+++ b/theories/Reification.v
@@ -11,8 +11,8 @@
 
 
 From ATBR Require Import Common Classes.
-From Coq Require Import FMapPositive.
-From Coq Require Import Eqdep.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import Eqdep.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/SemiRing.v b/theories/SemiRing.v
index 451eb02..9feb2ab 100644
--- a/theories/SemiRing.v
+++ b/theories/SemiRing.v
@@ -906,4 +906,3 @@ Goal forall `{KA: KleeneAlgebra} A (x y z: X A A), x+y==z*z -> sum 6 8 (fun _ =>
   setoid_rewrite H.
 Abort.
 endtests*)
-
diff --git a/theories/StrictStarForm.v b/theories/StrictStarForm.v
index a332d61..79be291 100644
--- a/theories/StrictStarForm.v
+++ b/theories/StrictStarForm.v
@@ -24,7 +24,7 @@ From ATBR Require Import KleeneAlgebra.
 From ATBR Require Import Model_RegExp. 
 Import RegExp.Load.
 From ATBR Require Reification.
-From Coq Require Import Bool.
+From Stdlib Require Import Bool.
 
 Open Scope lazy_bool_scope.
 
diff --git a/theories/Utils_WF.v b/theories/Utils_WF.v
index 3828b81..abb3d4a 100644
--- a/theories/Utils_WF.v
+++ b/theories/Utils_WF.v
@@ -217,7 +217,7 @@ End powerfix.
 (** Another way to construct well-founded relations: start with a well-founded one (e.g., the empty one), 
    and progressively add pairs satisfying some acyclicity property w.r.t. the current relation *)
 
-From Coq Require Relations.
+From Stdlib Require Relations.
 
 Section add_pair.
   Import Relations.