Adapt to rocq-prover/rocq#21851

Author: proux01

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"

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.
-

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.

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.
 

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.

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.
 

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.
-

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.
 

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.

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 :=