diff --git a/src/Rewriter/Demo.v b/src/Rewriter/Demo.v
index be6cc85b0..d7e8e102c 100644
--- a/src/Rewriter/Demo.v
+++ b/src/Rewriter/Demo.v
@@ -9,7 +9,7 @@ Require Import Rewriter.Util.plugins.RewriterBuild.
 (** We will be working with examples involving arithmetic on [nat] and
     [Z], as well as some examples on [list], so we import the relevant
     files. *)
-From Coq Require Import Arith ZArith List.
+From Stdlib Require Import Arith ZArith List.
 Import ListNotations. Local Open Scope list_scope.
 
 (** We [Unset Ltac Backtrace] to get prettier error messages. *)
diff --git a/src/Rewriter/Language/IdentifiersBasicGenerate.v b/src/Rewriter/Language/IdentifiersBasicGenerate.v
index 1d84bfe55..31447b7e7 100644
--- a/src/Rewriter/Language/IdentifiersBasicGenerate.v
+++ b/src/Rewriter/Language/IdentifiersBasicGenerate.v
@@ -1,7 +1,7 @@
-From Coq Require Import ZArith.
-From Coq Require Import Bool.
-From Coq Require Import Morphisms.
-From Coq Require Import List.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Bool.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import List.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Bool.
 Require Import Ltac2.Printf.
@@ -30,7 +30,7 @@ Require Import Rewriter.Util.Tactics.PrintGoal.
 Require Import Rewriter.Util.Tactics.CacheTerm.
 Require Import Rewriter.Util.Tactics2.Notations.
 Require Import Rewriter.Util.HProp.
-Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
 
 Import EqNotations.
 Module Compilers.
diff --git a/src/Rewriter/Language/IdentifiersGenerate.v b/src/Rewriter/Language/IdentifiersGenerate.v
index 037e95798..1dd2920c2 100644
--- a/src/Rewriter/Language/IdentifiersGenerate.v
+++ b/src/Rewriter/Language/IdentifiersGenerate.v
@@ -1,8 +1,8 @@
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import MSetPositive.
-From Coq Require Import List.
-From Coq Require Import Derive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import List.
+From Stdlib Require Import Derive.
 Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.PrimitiveSigma.
diff --git a/src/Rewriter/Language/IdentifiersGenerateProofs.v b/src/Rewriter/Language/IdentifiersGenerateProofs.v
index 73af83f7a..7747c47ec 100644
--- a/src/Rewriter/Language/IdentifiersGenerateProofs.v
+++ b/src/Rewriter/Language/IdentifiersGenerateProofs.v
@@ -1,6 +1,6 @@
-From Coq Require Import ZArith.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Util.PrimitiveSigma.
 Require Import Rewriter.Util.MSetPositive.Facts.
 Require Import Rewriter.Util.CPSNotations.
diff --git a/src/Rewriter/Language/IdentifiersLibrary.v b/src/Rewriter/Language/IdentifiersLibrary.v
index 5fd5aa29c..1930e0d19 100644
--- a/src/Rewriter/Language/IdentifiersLibrary.v
+++ b/src/Rewriter/Language/IdentifiersLibrary.v
@@ -1,9 +1,9 @@
-From Coq Require Import Bool.
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import MSetPositive.
-From Coq Require Import List.
-From Coq Require Import Derive.
+From Stdlib Require Import Bool.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import List.
+From Stdlib Require Import Derive.
 Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.PrimitiveSigma.
diff --git a/src/Rewriter/Language/IdentifiersLibraryProofs.v b/src/Rewriter/Language/IdentifiersLibraryProofs.v
index c763cb1c0..1627f3067 100644
--- a/src/Rewriter/Language/IdentifiersLibraryProofs.v
+++ b/src/Rewriter/Language/IdentifiersLibraryProofs.v
@@ -1,6 +1,6 @@
-From Coq Require Import ZArith.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Util.PrimitiveSigma.
 Require Import Rewriter.Util.MSetPositive.Facts.
 Require Import Rewriter.Util.CPSNotations.
diff --git a/src/Rewriter/Language/Language.v b/src/Rewriter/Language/Language.v
index 5eb8c287d..817748760 100644
--- a/src/Rewriter/Language/Language.v
+++ b/src/Rewriter/Language/Language.v
@@ -1,9 +1,9 @@
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import Bool.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
 Require Import Rewriter.Language.PreCommon.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.ListUtil.
@@ -17,7 +17,7 @@ Require Import Rewriter.Util.Bool.
 Require Import Rewriter.Util.ListUtil.
 Require Import Rewriter.Util.Prod.
 Require Import Rewriter.Util.Notations.
-Import Coq.Lists.List ListNotations.
+Import Stdlib.Lists.List ListNotations.
 Export Language.PreCommon.
 
 Local Set Primitive Projections.
diff --git a/src/Rewriter/Language/PreLemmas.v b/src/Rewriter/Language/PreLemmas.v
index 4a82a4aaf..7d0c0ba4d 100644
--- a/src/Rewriter/Language/PreLemmas.v
+++ b/src/Rewriter/Language/PreLemmas.v
@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Stdlib Require Import List.
 Require Import Rewriter.Language.Pre.
 Require Import Rewriter.Util.Bool.
 Require Import Rewriter.Util.NatUtil.
diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v
index e97ea6b7a..a95537221 100644
--- a/src/Rewriter/Language/Reify.v
+++ b/src/Rewriter/Language/Reify.v
@@ -1,9 +1,9 @@
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import Bool.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Printf.
 Require Import Rewriter.Language.PreCommon.
@@ -36,7 +36,7 @@ Require Import Rewriter.Util.Tactics2.DestCase.
 Require Import Rewriter.Util.Tactics2.InstantiateEvar.
 Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations.
 Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance.
-Import Coq.Lists.List ListNotations.
+Import Stdlib.Lists.List ListNotations.
 Export Language.PreCommon.
 
 Local Set Primitive Projections.
diff --git a/src/Rewriter/Language/UnderLetsProofs.v b/src/Rewriter/Language/UnderLetsProofs.v
index 95b213257..7e05665da 100644
--- a/src/Rewriter/Language/UnderLetsProofs.v
+++ b/src/Rewriter/Language/UnderLetsProofs.v
@@ -1,6 +1,6 @@
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import SetoidList.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import SetoidList.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
@@ -15,7 +15,7 @@ Require Import Rewriter.Util.Tactics.SpecializeAllWays.
 Require Import Rewriter.Util.Tactics.SpecializeBy.
 Require Import Rewriter.Util.Tactics.SplitInContext.
 Require Import Rewriter.Util.Tactics.SetoidSubst.
-Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
 
 Import EqNotations.
 Module Compilers.
diff --git a/src/Rewriter/Language/Wf.v b/src/Rewriter/Language/Wf.v
index 5a092ca58..89dc6ec44 100644
--- a/src/Rewriter/Language/Wf.v
+++ b/src/Rewriter/Language/Wf.v
@@ -1,9 +1,9 @@
-From Coq Require Import ZArith.
-From Coq Require Import List.
-From Coq Require Import Lia.
-From Coq Require Import FMapPositive.
-From Coq Require Import Morphisms.
-From Coq Require Import Relations.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import List.
+From Stdlib Require Import Lia.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relations.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Util.Tactics.BreakMatch.
@@ -29,7 +29,7 @@ Require Import Rewriter.Util.Equality.
 Require Import Rewriter.Util.IffT.
 Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.Notations.
-Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
 
 Import EqNotations.
 Module Compilers.
diff --git a/src/Rewriter/Rewriter/AllTactics.v b/src/Rewriter/Rewriter/AllTactics.v
index 1eb3be5b9..cbfedba0a 100644
--- a/src/Rewriter/Rewriter/AllTactics.v
+++ b/src/Rewriter/Rewriter/AllTactics.v
@@ -1,4 +1,4 @@
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 Require Import Rewriter.Language.Pre.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
diff --git a/src/Rewriter/Rewriter/Examples.v b/src/Rewriter/Rewriter/Examples.v
index d142cf889..0ac2ef60d 100644
--- a/src/Rewriter/Rewriter/Examples.v
+++ b/src/Rewriter/Rewriter/Examples.v
@@ -1,7 +1,7 @@
 (** * Examples of Using the Rewriter *)
-From Coq Require Import ZArith.
-From Coq Require Import Lia.
-From Coq Require Import List.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.ListUtil.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.Notations.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
index 519251f9d..a3b103c11 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
@@ -1,10 +1,10 @@
-From Coq Require Import QArith.
-From Coq Require Import Orders.
-From Coq Require Import Lia.
-From Coq Require Import Bool.
-From Coq Require Import Mergesort.
-From Coq Require Export List.
-From Coq Require Export ZArith.
+From Stdlib Require Import QArith.
+From Stdlib Require Import Orders.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Bool.
+From Stdlib Require Import Mergesort.
+From Stdlib Require Export List.
+From Stdlib Require Export ZArith.
 Export ListNotations.
 
 Global Set Printing Width 1000.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v b/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
index ff6da5043..8337e9b4f 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
@@ -1,10 +1,10 @@
-From Coq Require Import String.
-From Coq Require Import Lia.
-From Coq Require Import ZArith.
-From Coq Require Import QArith.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Import List.
+From Stdlib Require Import String.
+From Stdlib Require Import Lia.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import QArith.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Rewriter.Rewriter.Examples.PerfTesting.Sample.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v b/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
index 28aa7d58b..142f0b2b6 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
@@ -1,6 +1,6 @@
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
 
 Global Instance list_rect_Proper_dep_gen {A P} (RP : forall x : list A, P x -> P x -> Prop)
   : Proper (RP nil ==> forall_relation (fun x => forall_relation (fun xs => RP xs ==> RP (cons x xs))) ==> forall_relation RP) (@list_rect A P) | 10.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
index dd6f4e22e..60849bcc2 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
@@ -1,10 +1,10 @@
-From Coq Require Import Lia.
-From Coq Require Import ZArith.
-From Coq Require Import QArith.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Import String.
-From Coq Require Import List.
+From Stdlib Require Import Lia.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import QArith.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import String.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Import Rewriter.Util.plugins.RewriterBuild.
@@ -421,7 +421,7 @@ Ltac describe_goal nm :=
 
 Ltac do_coq_rewrite _ := rewrite -> !Z.add_0_r.
 
-From Coq Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Ltac do_ssr_rewrite _ := rewrite !Z.add_0_r.
 
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
index 3078cd58c..ca4d59869 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
@@ -1,14 +1,14 @@
 (** Utility file for subsampling large distributions *)
-From Coq Require Import String.
-From Coq Require Import Orders.
-From Coq Require Import Lia.
-From Coq Require Import Bool.
-From Coq Require Import Mergesort.
-From Coq Require Import QArith Qround Qabs Qminmax.
-From Coq Require Import NArith.
-From Coq Require Import ZArith.
-From Coq Require Import Arith.
-From Coq Require Import List.
+From Stdlib Require Import String.
+From Stdlib Require Import Orders.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Bool.
+From Stdlib Require Import Mergesort.
+From Stdlib Require Import QArith Qround Qabs Qminmax.
+From Stdlib Require Import NArith.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Arith.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.LetIn.
 Import ListNotations.
 Local Open Scope list_scope.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v b/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
index b91c6a68d..fb8dbea7d 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
@@ -1,10 +1,10 @@
-From Coq Require Import QArith.
-From Coq Require Import MSetPositive.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Export ZArith.
-From Coq Require Import List.
-From Coq Require Import String.
+From Stdlib Require Import QArith.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Export ZArith.
+From Stdlib Require Import List.
+From Stdlib Require Import String.
 Require Import Rewriter.Util.Prod.
 Require Import Rewriter.Util.Bool.Reflect.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v b/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
index 5c72d4fea..d8110f567 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
@@ -1,10 +1,10 @@
-From Coq Require Import Lia.
-From Coq Require Import ZArith.
-From Coq Require Import QArith.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Import List.
-From Coq Require Import String.
+From Stdlib Require Import Lia.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import QArith.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import List.
+From Stdlib Require Import String.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Import Rewriter.Util.plugins.RewriterBuild.
diff --git a/src/Rewriter/Rewriter/Examples/PrefixSums.v b/src/Rewriter/Rewriter/Examples/PrefixSums.v
index e4afe7b0f..bdcab5cd0 100644
--- a/src/Rewriter/Rewriter/Examples/PrefixSums.v
+++ b/src/Rewriter/Rewriter/Examples/PrefixSums.v
@@ -1,8 +1,8 @@
 (** * Examples of Using the Rewriter *)
-From Coq Require Import Lia.
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Import List.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.Notations.
 Require Import Rewriter.Util.NatUtil.
diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v
index b225f6720..fc54d4986 100644
--- a/src/Rewriter/Rewriter/InterpProofs.v
+++ b/src/Rewriter/Rewriter/InterpProofs.v
@@ -1,10 +1,10 @@
-From Coq Require Import ZArith.
-From Coq Require Import Lia.
-From Coq Require Import SetoidList.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
diff --git a/src/Rewriter/Rewriter/ProofsCommon.v b/src/Rewriter/Rewriter/ProofsCommon.v
index 7e93b687b..947132a54 100644
--- a/src/Rewriter/Rewriter/ProofsCommon.v
+++ b/src/Rewriter/Rewriter/ProofsCommon.v
@@ -1,11 +1,11 @@
-From Coq Require Import ZArith.
-From Coq Require Import Lia.
-From Coq Require Import SetoidList.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
-From Coq.Program Require Import Tactics.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import Program.Tactics.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
@@ -44,7 +44,7 @@ Require Import Rewriter.Util.Bool.
 Require Import Rewriter.Util.NatUtil.
 Require Rewriter.Util.InductiveHList.
 Require Rewriter.Util.PrimitiveHList.
-Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
index 8e136624d..c326e4887 100644
--- a/src/Rewriter/Rewriter/ProofsCommonTactics.v
+++ b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -1,10 +1,10 @@
-From Coq Require Import ZArith.
-From Coq Require Import Lia.
-From Coq Require Import SetoidList.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
@@ -42,7 +42,7 @@ Require Import Rewriter.Util.Decidable.
 Require Import Rewriter.Util.Bool.
 Require Import Rewriter.Util.NatUtil.
 Require Rewriter.Util.PrimitiveHList.
-Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/Rewriter/Rewriter/Reify.v b/src/Rewriter/Rewriter/Reify.v
index 52ae672e2..de9cfdfbd 100644
--- a/src/Rewriter/Rewriter/Reify.v
+++ b/src/Rewriter/Rewriter/Reify.v
@@ -1,7 +1,7 @@
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import MSetPositive.
-From Coq Require Import List.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import List.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Printf.
 Require Import Ltac2.Bool.
diff --git a/src/Rewriter/Rewriter/Rewriter.v b/src/Rewriter/Rewriter/Rewriter.v
index b56ded7e6..32502698d 100644
--- a/src/Rewriter/Rewriter/Rewriter.v
+++ b/src/Rewriter/Rewriter/Rewriter.v
@@ -1,7 +1,7 @@
-From Coq Require Import ZArith.
-From Coq Require Import FMapPositive.
-From Coq Require Import MSetPositive.
-From Coq Require Import List.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import FMapPositive.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import List.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.UnderLets.
 Require Import Rewriter.Language.IdentifiersLibrary.
diff --git a/src/Rewriter/Rewriter/Wf.v b/src/Rewriter/Rewriter/Wf.v
index 4cf6d558b..3bb90decc 100644
--- a/src/Rewriter/Rewriter/Wf.v
+++ b/src/Rewriter/Rewriter/Wf.v
@@ -1,9 +1,9 @@
-From Coq Require Import ZArith.
-From Coq Require Import Lia.
-From Coq Require Import List.
-From Coq Require Import Morphisms.
-From Coq Require Import MSetPositive.
-From Coq Require Import FMapPositive.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Lia.
+From Stdlib Require Import List.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
@@ -27,7 +27,7 @@ Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.HProp.
 Require Import Rewriter.Util.Decidable.
 Require Import Rewriter.Util.Bool.Reflect.
-Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
+Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/Rewriter/Util/Bool.v b/src/Rewriter/Util/Bool.v
index 97e25cc27..8f1d30abe 100644
--- a/src/Rewriter/Util/Bool.v
+++ b/src/Rewriter/Util/Bool.v
@@ -1,6 +1,6 @@
 (*** Boolean Utility Lemmas and Databases *)
-From Coq Require Import Bool.
-From Coq Require Import Morphisms.
+From Stdlib Require Import Bool.
+From Stdlib Require Import Morphisms.
 
 (* We would use [Scheme Minimality for bool Sort Type.], but we want
    [bool_rect_nodep] to unfold directly to [bool_rect] so that
diff --git a/src/Rewriter/Util/Bool/Equality.v b/src/Rewriter/Util/Bool/Equality.v
index 122d8632b..b38ce65fb 100644
--- a/src/Rewriter/Util/Bool/Equality.v
+++ b/src/Rewriter/Util/Bool/Equality.v
@@ -1,3 +1,3 @@
-From Coq Require Import Bool.
+From Stdlib Require Import Bool.
 
 Scheme Equality for bool.
diff --git a/src/Rewriter/Util/Bool/Reflect.v b/src/Rewriter/Util/Bool/Reflect.v
index 6dd39dbd1..589d6fd27 100644
--- a/src/Rewriter/Util/Bool/Reflect.v
+++ b/src/Rewriter/Util/Bool/Reflect.v
@@ -1,12 +1,12 @@
 (** * Some lemmas about [Bool.reflect] *)
-From Coq Require Import CMorphisms.
-From Coq Require Import String.
-From Coq Require Import Ascii.
-From Coq Require Import Bool.
-From Coq Require Import RelationClasses.
-From Coq Require Import Arith.
-From Coq Require Import BinInt ZArith_dec.
-From Coq Require Import BinNat.
+From Stdlib Require Import CMorphisms.
+From Stdlib Require Import String.
+From Stdlib Require Import Ascii.
+From Stdlib Require Import Bool.
+From Stdlib Require Import RelationClasses.
+From Stdlib Require Import Arith.
+From Stdlib Require Import BinInt ZArith_dec.
+From Stdlib Require Import BinNat.
 Require Import Rewriter.Util.HProp.
 Require Import Rewriter.Util.Decidable.
 Require Import Rewriter.Util.Prod.
diff --git a/src/Rewriter/Util/Decidable.v b/src/Rewriter/Util/Decidable.v
index a4e951dcc..831537426 100644
--- a/src/Rewriter/Util/Decidable.v
+++ b/src/Rewriter/Util/Decidable.v
@@ -1,12 +1,12 @@
 (** Typeclass for decidable propositions *)
 
-From Coq Require Import Eqdep_dec.
-From Coq Require Import List.
+From Stdlib Require Import Eqdep_dec.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.FixCoqMistakes.
 Require Import Rewriter.Util.Sigma.
 Require Import Rewriter.Util.HProp.
-From Coq Require Import BinInt ZArith_dec.
-From Coq Require Import BinNat.
+From Stdlib Require Import BinInt ZArith_dec.
+From Stdlib Require Import BinNat.
 
 Local Open Scope type_scope.
 
diff --git a/src/Rewriter/Util/Equality.v b/src/Rewriter/Util/Equality.v
index 780cd0e75..55e5c7677 100644
--- a/src/Rewriter/Util/Equality.v
+++ b/src/Rewriter/Util/Equality.v
@@ -4,7 +4,7 @@
     [eq].  We build up enough lemmas about this structure to deal
     nicely with proofs of equality that come up in practice in this
     project. *)
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 Require Import Rewriter.Util.Isomorphism.
 Require Import Rewriter.Util.HProp.
 
diff --git a/src/Rewriter/Util/FMapPositive/Equality.v b/src/Rewriter/Util/FMapPositive/Equality.v
index fb0e41425..930272d19 100644
--- a/src/Rewriter/Util/FMapPositive/Equality.v
+++ b/src/Rewriter/Util/FMapPositive/Equality.v
@@ -1,4 +1,4 @@
-From Coq Require Import FMapPositive.
+From Stdlib Require Import FMapPositive.
 Require Import Rewriter.Util.Bool.Equality.
 Require Import Rewriter.Util.Decidable.
 
diff --git a/src/Rewriter/Util/FixCoqMistakes.v b/src/Rewriter/Util/FixCoqMistakes.v
index 8a3a94313..cd62b6ccc 100644
--- a/src/Rewriter/Util/FixCoqMistakes.v
+++ b/src/Rewriter/Util/FixCoqMistakes.v
@@ -1,5 +1,5 @@
 (** * Fixes *)
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 Require Export Rewriter.Util.GlobalSettings.
 
 (** Coq is poorly designed in some ways.  We fix some of these issues
@@ -30,7 +30,7 @@ Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H :
      end.
 
 (** Implement the fix in https://github.com/coq/coq/pull/10966, even though it doesn't land until 8.11 *)
-Ltac Coq.Init.Tactics.assert_fails tac ::=
+Ltac Corelib.Init.Tactics.assert_fails tac ::=
   tryif (cut True; [ intros _; once tac | ]) then fail 0 tac "succeeds" else idtac.
 
 (** Work around BZ#5341, https://coq.inria.fr/bugs/show_bug.cgi?id=5341, [subst] fails with bogus error message about universe polymorphism *)
diff --git a/src/Rewriter/Util/IffT.v b/src/Rewriter/Util/IffT.v
index 911b204a9..8a0faeb71 100644
--- a/src/Rewriter/Util/IffT.v
+++ b/src/Rewriter/Util/IffT.v
@@ -1,4 +1,4 @@
-From Coq Require Import RelationClasses.
+From Corelib Require Import RelationClasses.
 Notation iffT A B := (((A -> B) * (B -> A)))%type.
 Notation iffTp := (fun A B => inhabited (iffT A B)).
 
diff --git a/src/Rewriter/Util/LetIn.v b/src/Rewriter/Util/LetIn.v
index cb7ae3a98..ab56c24ee 100644
--- a/src/Rewriter/Util/LetIn.v
+++ b/src/Rewriter/Util/LetIn.v
@@ -1,5 +1,5 @@
 Require Import Rewriter.Util.FixCoqMistakes.
-From Coq Require Import Morphisms Relation_Definitions.
+From Stdlib Require Import Morphisms Relation_Definitions.
 Require Import Rewriter.Util.Tactics.GetGoal.
 Require Import Rewriter.Util.Notations.
 
diff --git a/src/Rewriter/Util/ListUtil.v b/src/Rewriter/Util/ListUtil.v
index 22f9f9807..3d5e4668e 100644
--- a/src/Rewriter/Util/ListUtil.v
+++ b/src/Rewriter/Util/ListUtil.v
@@ -1,10 +1,10 @@
-From Coq Require Import List.
-From Coq Require Import SetoidList.
-From Coq Require Import Lia.
-From Coq Require Import Peano_dec.
-From Coq Require Import ZArith.
-From Coq Require Import Arith.
-From Coq Require Import Morphisms.
+From Stdlib Require Import List.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Peano_dec.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Arith.
+From Stdlib Require Import Morphisms.
 Require Import Rewriter.Util.NatUtil.
 Require Import Rewriter.Util.Pointed.
 Require Import Rewriter.Util.Prod.
@@ -1977,7 +1977,7 @@ Qed.
 #[global] Hint Rewrite <- @firstn_update_nth : pull_firstn.
 #[global] Hint Rewrite <- @firstn_update_nth : push_update_nth.
 
-From Coq Require Import SetoidList.
+From Stdlib Require Import SetoidList.
 Global Instance Proper_nth_default : forall A eq,
   Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)).
 Proof.
diff --git a/src/Rewriter/Util/ListUtil/Forall.v b/src/Rewriter/Util/ListUtil/Forall.v
index 8f8004eef..b712f0b19 100644
--- a/src/Rewriter/Util/ListUtil/Forall.v
+++ b/src/Rewriter/Util/ListUtil/Forall.v
@@ -1,6 +1,6 @@
-From Coq Require Import Lia.
-From Coq Require Import Morphisms.
-From Coq Require Import List.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.Tactics.SpecializeBy.
 Require Import Rewriter.Util.Tactics.SplitInContext.
 Require Import Rewriter.Util.Tactics.DestructHead.
diff --git a/src/Rewriter/Util/ListUtil/SetoidList.v b/src/Rewriter/Util/ListUtil/SetoidList.v
index 62a2e70e2..ba037f773 100644
--- a/src/Rewriter/Util/ListUtil/SetoidList.v
+++ b/src/Rewriter/Util/ListUtil/SetoidList.v
@@ -1,6 +1,6 @@
-From Coq Require Import List.
-From Coq Require Import Setoid.
-From Coq Require Import SetoidList.
+From Stdlib Require Import List.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import SetoidList.
 Require Import Rewriter.Util.Option.
 
 Import ListNotations.
diff --git a/src/Rewriter/Util/Logic/ExistsEqAnd.v b/src/Rewriter/Util/Logic/ExistsEqAnd.v
index fa41d2993..f623c8113 100644
--- a/src/Rewriter/Util/Logic/ExistsEqAnd.v
+++ b/src/Rewriter/Util/Logic/ExistsEqAnd.v
@@ -1,4 +1,4 @@
-From Coq Require Import Setoid.
+From Stdlib Require Import Setoid.
 Require Import Rewriter.Util.FixCoqMistakes.
 Require Import Rewriter.Util.Tactics.DestructHead.
 
diff --git a/src/Rewriter/Util/MSetPositive/Equality.v b/src/Rewriter/Util/MSetPositive/Equality.v
index 55f791112..fdd7d1749 100644
--- a/src/Rewriter/Util/MSetPositive/Equality.v
+++ b/src/Rewriter/Util/MSetPositive/Equality.v
@@ -1,4 +1,4 @@
-From Coq Require Import MSetPositive.
+From Stdlib Require Import MSetPositive.
 Require Import Rewriter.Util.Bool.Equality.
 Require Import Rewriter.Util.Decidable.
 
diff --git a/src/Rewriter/Util/MSetPositive/Facts.v b/src/Rewriter/Util/MSetPositive/Facts.v
index 56dfc182c..3a2da8ad0 100644
--- a/src/Rewriter/Util/MSetPositive/Facts.v
+++ b/src/Rewriter/Util/MSetPositive/Facts.v
@@ -1,9 +1,9 @@
-From Coq Require Import Setoid.
-From Coq Require Import Morphisms.
-From Coq Require Import List.
-From Coq Require Import SetoidList.
-From Coq Require Import MSetPositive.
-From Coq Require Import MSetFacts.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import List.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import MSetPositive.
+From Stdlib Require Import MSetFacts.
 Require Import Rewriter.Util.Tactics.BreakMatch.
 Require Import Rewriter.Util.Tactics.SplitInContext.
 Require Import Rewriter.Util.Tactics.SpecializeBy.
diff --git a/src/Rewriter/Util/NatUtil.v b/src/Rewriter/Util/NatUtil.v
index f0c6ba360..9083d8a23 100644
--- a/src/Rewriter/Util/NatUtil.v
+++ b/src/Rewriter/Util/NatUtil.v
@@ -1,9 +1,9 @@
-From Coq Require Eqdep_dec.
-From Coq Require Import NArith.
-From Coq Require Import Arith.
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
-From Coq Require Import Lia.
+From Stdlib Require Eqdep_dec.
+From Stdlib Require Import NArith.
+From Stdlib Require Import Arith.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import Lia.
 Import Nat.
 
 Scheme Equality for nat.
diff --git a/src/Rewriter/Util/Option.v b/src/Rewriter/Util/Option.v
index fc70d67b6..6bfdbe95b 100644
--- a/src/Rewriter/Util/Option.v
+++ b/src/Rewriter/Util/Option.v
@@ -1,5 +1,5 @@
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
 Require Import Rewriter.Util.Tactics.BreakMatch.
 Require Import Rewriter.Util.Tactics.DestructHead.
 Require Import Rewriter.Util.Notations.
diff --git a/src/Rewriter/Util/OptionList.v b/src/Rewriter/Util/OptionList.v
index a2b34589f..b54a2c868 100644
--- a/src/Rewriter/Util/OptionList.v
+++ b/src/Rewriter/Util/OptionList.v
@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.Notations.
 
diff --git a/src/Rewriter/Util/Pointed.v b/src/Rewriter/Util/Pointed.v
index a33b1906e..2ae7456ce 100644
--- a/src/Rewriter/Util/Pointed.v
+++ b/src/Rewriter/Util/Pointed.v
@@ -1,4 +1,4 @@
-From Coq Require Import BinNums.
+From Stdlib Require Import BinNums.
 
 Local Generalizable All Variables.
 
diff --git a/src/Rewriter/Util/PrimitiveHList.v b/src/Rewriter/Util/PrimitiveHList.v
index 1a1ffba81..792b26cd0 100644
--- a/src/Rewriter/Util/PrimitiveHList.v
+++ b/src/Rewriter/Util/PrimitiveHList.v
@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Stdlib Require Import List.
 Require Import Rewriter.Util.PrimitiveProd.
 
 Import Primitive.Notations.
diff --git a/src/Rewriter/Util/PrimitiveProd.v b/src/Rewriter/Util/PrimitiveProd.v
index ab3f6d812..ea87ee65e 100644
--- a/src/Rewriter/Util/PrimitiveProd.v
+++ b/src/Rewriter/Util/PrimitiveProd.v
@@ -5,7 +5,7 @@
     between two such pairs, or when we want such an equality, we have
     a systematic way of reducing such equalities to equalities at
     simpler types. *)
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 Require Import Rewriter.Util.IffT.
 Require Import Rewriter.Util.Equality.
 Require Import Rewriter.Util.GlobalSettings.
diff --git a/src/Rewriter/Util/PrimitiveSigma.v b/src/Rewriter/Util/PrimitiveSigma.v
index 81010e633..c8a068f49 100644
--- a/src/Rewriter/Util/PrimitiveSigma.v
+++ b/src/Rewriter/Util/PrimitiveSigma.v
@@ -5,7 +5,7 @@
     two such pairs, or when we want such an equality, we have a
     systematic way of reducing such equalities to equalities at
     simpler types. *)
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 Require Import Rewriter.Util.IffT.
 Require Import Rewriter.Util.Equality.
 Require Import Rewriter.Util.GlobalSettings.
diff --git a/src/Rewriter/Util/Prod.v b/src/Rewriter/Util/Prod.v
index d8f7b1005..dad31817f 100644
--- a/src/Rewriter/Util/Prod.v
+++ b/src/Rewriter/Util/Prod.v
@@ -5,9 +5,9 @@
     between two such pairs, or when we want such an equality, we have
     a systematic way of reducing such equalities to equalities at
     simpler types. *)
-From Coq Require Import Morphisms.
-From Coq Require Import Setoid.
-From Coq Require Import Bool.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import Bool.
 Require Import Rewriter.Util.IffT.
 Require Import Rewriter.Util.Equality.
 Require Import Rewriter.Util.GlobalSettings.
diff --git a/src/Rewriter/Util/Sigma/Related.v b/src/Rewriter/Util/Sigma/Related.v
index 0d72483de..e2de73bce 100644
--- a/src/Rewriter/Util/Sigma/Related.v
+++ b/src/Rewriter/Util/Sigma/Related.v
@@ -1,6 +1,6 @@
-From Coq Require Import RelationClasses.
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import RelationClasses.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
 Import EqNotations.
 
 Definition related_sigT_by_eq {A P1 P2} (R : forall x : A, P1 x -> P2 x -> Prop)
diff --git a/src/Rewriter/Util/Strings/Ascii.v b/src/Rewriter/Util/Strings/Ascii.v
index b32a84781..b1e5cf2a9 100644
--- a/src/Rewriter/Util/Strings/Ascii.v
+++ b/src/Rewriter/Util/Strings/Ascii.v
@@ -1,5 +1,5 @@
-From Coq Require Import NArith.
-From Coq Require Import Ascii.
+From Stdlib Require Import NArith.
+From Stdlib Require Import Ascii.
 Require Import Rewriter.Util.Notations.
 
 Local Open Scope bool_scope.
diff --git a/src/Rewriter/Util/Strings/Decimal.v b/src/Rewriter/Util/Strings/Decimal.v
index af6a71dd6..982fa4570 100644
--- a/src/Rewriter/Util/Strings/Decimal.v
+++ b/src/Rewriter/Util/Strings/Decimal.v
@@ -1,8 +1,8 @@
-From Coq Require Import Ascii String.
-From Coq Require Import BinNums.
-From Coq Require Import DecimalString.
-From Coq Require DecimalN.
-From Coq Require DecimalZ.
+From Stdlib Require Import Ascii String.
+From Stdlib Require Import BinNums.
+From Stdlib Require Import DecimalString.
+From Stdlib Require DecimalN.
+From Stdlib Require DecimalZ.
 Import BinPosDef.
 Import BinIntDef.
 Import BinNatDef.
diff --git a/src/Rewriter/Util/Strings/Parse/Common.v b/src/Rewriter/Util/Strings/Parse/Common.v
index 1adf06c20..f24dc585e 100644
--- a/src/Rewriter/Util/Strings/Parse/Common.v
+++ b/src/Rewriter/Util/Strings/Parse/Common.v
@@ -1,4 +1,4 @@
-From Coq Require Import Ascii String List.
+From Stdlib Require Import Ascii String List.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.Strings.String.
 Require Import Rewriter.Util.Notations.
diff --git a/src/Rewriter/Util/Strings/ParseArithmetic.v b/src/Rewriter/Util/Strings/ParseArithmetic.v
index 7f6dc8dbf..97df0bd2f 100644
--- a/src/Rewriter/Util/Strings/ParseArithmetic.v
+++ b/src/Rewriter/Util/Strings/ParseArithmetic.v
@@ -1,11 +1,11 @@
-From Coq Require Import Ascii String List.
-From Coq Require Import BinNums.
-From Coq Require Import QArith.
-From Coq Require Import ZArith.
+From Stdlib Require Import Ascii String List.
+From Stdlib Require Import BinNums.
+From Stdlib Require Import QArith.
+From Stdlib Require Import ZArith.
 Require Import Rewriter.Util.Option.
-From Coq Require BinaryString.
-From Coq Require OctalString.
-From Coq Require HexString.
+From Stdlib Require BinaryString.
+From Stdlib Require OctalString.
+From Stdlib Require HexString.
 Require Import Rewriter.Util.Strings.Decimal.
 Require Import Rewriter.Util.Strings.Parse.Common.
 Require Import Rewriter.Util.Notations.
diff --git a/src/Rewriter/Util/Strings/String.v b/src/Rewriter/Util/Strings/String.v
index d9da2bb78..57f3f7b24 100644
--- a/src/Rewriter/Util/Strings/String.v
+++ b/src/Rewriter/Util/Strings/String.v
@@ -1,7 +1,7 @@
-From Coq Require Import PeanoNat.
-From Coq Require Import Lia.
-From Coq Require Import String.
-From Coq Require Import Ascii.
+From Stdlib Require Import PeanoNat.
+From Stdlib Require Import Lia.
+From Stdlib Require Import String.
+From Stdlib Require Import Ascii.
 Require Import Rewriter.Util.Strings.Ascii.
 
 Local Open Scope list_scope.
diff --git a/src/Rewriter/Util/Sum.v b/src/Rewriter/Util/Sum.v
index 086b8e10a..d128e2663 100644
--- a/src/Rewriter/Util/Sum.v
+++ b/src/Rewriter/Util/Sum.v
@@ -1,5 +1,5 @@
-From Coq Require Import Morphisms.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Morphisms.
+From Stdlib Require Import Relation_Definitions.
 Require Import Rewriter.Util.Decidable.
 Require Import Rewriter.Util.Tactics.DestructHead.
 Require Import Rewriter.Util.Tactics.SetoidSubst.