Adapt to https://github.com/rocq-prover/rocq/pull/21851

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.
 
@@ -147,7 +147,7 @@
 Lemma le_lt_bool_false : forall x y, le_lt_bool x y = false <-> y < x. 
 Proof. intros. nat_analyse; intuition. lia. Qed.
 
 #[global] Hint Rewrite eq_nat_bool_true eq_nat_bool_false le_lt_bool_true le_lt_bool_false : nat_prop.
 Ltac nat_prop := autorewrite with nat_prop in *.
 
 
@@ -160,7 +160,7 @@
       The database bool_simpl should be enriched with lemmas such as [forall x, eqb x x = true], 
       which is done in Numbers.v
 *)
 #[global] Hint Rewrite 
   orb_false_r                    (** b || false -> b *)
   orb_false_l                    (** false || b -> b *)
   orb_true_r                     (** b || true  -> true *)
@@ -212,7 +212,7 @@
 Lemma eq_not_negb  : forall b c, b = c <-> ~ (b = negb c). 
 Proof. intros [|] [|]; firstorder; simpl; try congruence. Qed.
 
 #[global] Hint Rewrite andb_false_iff andb_true_iff orb_false_iff orb_true_iff negb_true negb_false : bool_connectors.
 
 Ltac bool_connectors := autorewrite with bool_connectors in *.
 
@@ -256,4 +256,3 @@
     | [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.
 
@@ -62,7 +62,7 @@
 
 Ltac rsimpl := simpl; autorewrite with simpl using ti_auto.
 
 #[global] Hint Extern 9 (@eq nat ?x ?y) => abstract lia: lia.
 #[global] Hint Extern 9 (Peano.le ?x ?y) => abstract lia: lia.
 #[global] Hint Extern 9 (Peano.lt ?x ?y) => abstract lia: lia.
 

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

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

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.
 

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

theories/Model_Relations.v

@@ -146,4 +146,3 @@ Module Load.
               change rel_star with (@star rel_Graph rel_Star_Op).
 
 End Load.
-

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.

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.

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.
 

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.
 
@@ -77,7 +77,7 @@
   Lemma mem_false_not_in: forall x s, mem x s = false <-> ~ In x s.
   Proof. intros. mem_analyse; intuition discriminate. Qed. 
 
   #[global] Hint Rewrite mem_false_not_in : mem_prop.
   #[global] Hint Rewrite <- mem_iff : mem_prop.
   Ltac mem_prop := autorewrite with mem_prop in *.
 
@@ -367,4 +367,3 @@
   Qed.
 
 End MySetProps.  
-

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).
@@ -35,7 +35,7 @@
 
  Parameter compare_sym : forall x y, (y?=x) = CompOpp (x?=y).
  Parameter compare_trans : forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
  Parameter reflect : forall x y, x ?= y = Eq -> x = y.
 End OrderedTypeAlt. 
 
 Module Nat_as_OTA <: OrderedTypeAlt.
@@ -233,4 +233,3 @@
 
 Module Nat_as_OT := OrderedType_from_Alt Nat_as_OTA.
 Module Pos_as_OT := OrderedType_from_Alt Pos_as_OTA.
-

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

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.

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*)
-

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.
 

theories/Utils_WF.v

@@ -111,7 +111,7 @@
 Section powerfix.
 
   Variables A B: Type.
   Notation Fun := (A -> B).
 
   (** the three following functions "iterate" their [f] argument lazily: iteration stops whenever [f] 
      no longer makes recursive calls.
@@ -217,7 +217,7 @@
 (** 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.