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

src/Extract.v

@@ -14,7 +14,7 @@
 (* 02110-1301 USA                                                     *)
 
 From Stalmarck Require Import algoRun.
-From Coq Require Import ZArith.
-From Coq Require Import Extraction.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Extraction.
 
 Extraction "stal.ml" run checkTracef zero Pos.of_succ_nat.

src/staltac_lib.ml

@@ -31,7 +31,7 @@ let global_reference_in_absolute_module dir id =
   Nametab.global_of_path (Libnames.make_path dir id)
 
 let constant dir s =
-  let dir = DirPath.make (List.map Id.of_string (List.rev ("Coq"::dir))) in
+  let dir = DirPath.make (List.map Id.of_string (List.rev ("Corelib"::dir))) in
   let id = Id.of_string s in
   try
     EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (global_reference_in_absolute_module dir id))

theories/Algorithm/BoolAux.v

@@ -21,7 +21,7 @@ Some standard properties of booleans.
 
 *)
 
-From Coq Require Export Bool.
+From Stdlib Require Export Bool.
 
 Lemma de_morgan1 : forall b1 b2 : bool, negb (b1 || b2) = negb b1 && negb b2.
 Proof.

theories/Algorithm/OrderedListEq.v

@@ -22,11 +22,11 @@ we took a special care so that every function can be evaluated
 inside Coq, see OrderedListEq_ex
 *)
 
-From Coq Require Import Arith.
-From Coq Require Export List.
-From Coq Require Import Lexicographic_Exponentiation.
-From Coq Require Export Relation_Definitions.
-From Coq Require Export Relation_Operators.
+From Stdlib Require Import Arith.
+From Stdlib Require Export List.
+From Stdlib Require Import Lexicographic_Exponentiation.
+From Stdlib Require Export Relation_Definitions.
+From Stdlib Require Export Relation_Operators.
 From Stalmarck Require Export sTactic.
 
 Section OrderedList.

theories/Algorithm/OrderedListEq_ex.v

@@ -21,7 +21,7 @@ How to use OrderedList
 *)
 
 From Stalmarck Require Import OrderedListEq.
-From Coq Require Import Arith. (* For Nat *)
+From Stdlib Require Import Arith. (* For Nat *)
 
 Definition CNat : forall a b : nat, {a < b} + {b < a} + {a = b}.
 fix CNat 1; intros a; case a; [ idtac | intros a' ]; intros b; case b;
@@ -58,7 +58,7 @@ Eval compute in (appnat l1 l2).
 Eval compute in (getminnat l1 l2).
 Eval compute in (internat l1 l2).
 
-From Coq Require Import ZArith. (* For Z *)
+From Stdlib Require Import ZArith. (* For Z *)
 
 Definition CZ : forall a b : Z, {(a < b)%Z} + {(b < a)%Z} + {a = b}.
 intros a b; CaseEq (a - b)%Z.

theories/Algorithm/PolyListAux.v

@@ -20,8 +20,8 @@ Pierre Letouzey & Laurent Thery
 Definition of rem a function that removes elt from polymorphic lists
 *)
 
-From Coq Require Import Arith.
-From Coq Require Import List.
+From Stdlib Require Import Arith.
+From Stdlib Require Import List.
 
 Section Auxrem.
 Variable A : Type.

theories/Algorithm/algoRun.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Some examples of computing with stalmarck inside Coq
 *)
 
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 From Stalmarck Require Export algoStalmarck.
 From Stalmarck Require Export algoTrace.
 From Stalmarck Require Export makeTriplet.

theories/Algorithm/complete.v

@@ -174,7 +174,7 @@ rewrite (Hab1 f Abs Hf2); rewrite (rZEvalCompInv b f).
 case (rZEval f b); auto with bool stalmarck.
 Qed.
 
-From Coq Require Import Arith.
+From Stdlib Require Import Arith.
 
 Fixpoint nthTail (n : nat) : list rZ -> list rZ :=
   fun l : list rZ =>

theories/Algorithm/equalBefore.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of equality on booleans up to a certain number
 *)
 
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Relation_Definitions.
 From Stalmarck Require Export triplet.
 
 (** f and g gives same value for rNat less than m *)

theories/Algorithm/interImplement2.v

@@ -23,7 +23,7 @@ Implement the intersection (2 files)
 From Stalmarck Require Import rZ.
 From Stalmarck Require Import OrderedListEq.
 From Stalmarck Require Import LetP.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Relation_Definitions.
 From Stalmarck Require Import state.
 From Stalmarck Require Import restrictState.
 From Stalmarck Require Import ltState.

theories/Algorithm/interImplement2_ex.v

@@ -21,7 +21,7 @@ How to use our module on ordered list
 *)
 
 From Stalmarck Require Import interImplement2.
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 
 #[local] Definition A := rArrayInit _ (fun n : rNat => class nil).
 

theories/Algorithm/interState.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of the intersection of two states
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export stateDec.
 
 (** The property of being an intersection *)

theories/Algorithm/ltState.v

@@ -22,11 +22,11 @@ of valid equations where variables belong to a given list
 *)
 
 From Stalmarck Require Import state.
-From Coq Require Import Arith.
+From Stdlib Require Import Arith.
 From Stalmarck Require Import stateDec.
-From Coq Require Import Inverse_Image.
-From Coq Require Import Compare.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Inverse_Image.
+From Stdlib Require Import Compare.
+From Stdlib Require Import Relation_Definitions.
 
 Section lt.
 Variable L : list rNat.

theories/Algorithm/rZ.v

@@ -31,12 +31,12 @@ At the end we define functional arrays that will be used in implementation
 *)
 
 From Stalmarck Require Import sTactic.
-From Coq Require Import Relation_Definitions.
-From Coq Require Import ZArith.
-From Coq Require Import Inverse_Image.
-From Coq Require Import Inclusion.
-From Coq Require Import Wf_nat.
-From Coq Require Import List.
+From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Inverse_Image.
+From Stdlib Require Import Inclusion.
+From Stdlib Require Import Wf_nat.
+From Stdlib Require Import List.
 
 Definition rNat := positive.
 

theories/Algorithm/refl.v

@@ -20,9 +20,9 @@ Pierre Letouzey & Laurent Thery
 Construct a function of type [Expr -> Prop]
 *)
 
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 From Stalmarck Require Import normalize.
-From Coq Require Import Classical.
+From Stdlib Require Import Classical.
 From Stalmarck Require Import sTactic.
 
 Section refl.

theories/Algorithm/state.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of states as the list of equations, i.e., pairs of rZ
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export triplet.
 
 Definition State := list (rZ * rZ).

theories/Algorithm/stateDec.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Given a state, equality is decidable
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export state.
 
 (** To show that the equality is decidable we need a more `constructive' predicate

theories/Algorithm/triplet.v

@@ -20,9 +20,9 @@ Pierre Letouzey & Laurent Thery
 Definition of triplets
 *)
 
-From Coq Require Export Bool.
+From Stdlib Require Export Bool.
 From Stalmarck Require Export rZ.
-From Coq Require Export List.
+From Stdlib Require Export List.
 From Stalmarck Require Export normalize.
 From Stalmarck Require Export sTactic.
 

theories/Algorithm/unionState.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of the union of two states
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export state.
 
 (** The property of being an union *)

theories/Algorithm/wfArray.v

@@ -22,10 +22,10 @@ Define a notion of wellformedness of function arrays for our application
 
 From Stalmarck Require Export rZ.
 From Stalmarck Require Export OrderedListEq.
-From Coq Require Export Relation_Definitions.
+From Stdlib Require Export Relation_Definitions.
 From Stalmarck Require Export LetP.
 From Stalmarck Require Export PolyListAux.
-From Coq Require Export List.
+From Stdlib Require Export List.
 From Stalmarck Require Export sTactic.
 
 (** Definition of well formed array and some properties *)

theories/Tactic/StalTac.v

@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 A wrapper for the stalmarck tactic
 *)
 
-From Coq Require Export ZArith.
+From Stdlib Require Export ZArith.
 From Stalmarck Require Export normalize.
 From Stalmarck Require Export algoTrace.
 From Stalmarck Require Export refl.

theories/Tactic/StalTac_ex.v

@@ -21,7 +21,7 @@ Examples for the stalmarck tactic
 *)
 
 From Stalmarck Require Import StalTac.
-From Coq Require Import Classical.
+From Stdlib Require Import Classical.
 
 Theorem Praeclarum :
  forall x y z t : Prop, (x -> z) /\ (y -> t) -> x /\ y -> z /\ t.