diff --git a/src/Rewriter/Demo.v b/src/Rewriter/Demo.v
index 39dedab8d..be6cc85b0 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. *)
-Require Import Coq.Arith.Arith Coq.ZArith.ZArith Coq.Lists.List.
+From Coq 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 c5128ea1d..edace12f8 100644
--- a/src/Rewriter/Language/IdentifiersBasicGenerate.v
+++ b/src/Rewriter/Language/IdentifiersBasicGenerate.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import Bool.
+From Coq Require Import Morphisms.
+From Coq Require Import List.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Bool.
 Require Import Ltac2.Printf.
diff --git a/src/Rewriter/Language/IdentifiersGenerate.v b/src/Rewriter/Language/IdentifiersGenerate.v
index b93250c2b..037e95798 100644
--- a/src/Rewriter/Language/IdentifiersGenerate.v
+++ b/src/Rewriter/Language/IdentifiersGenerate.v
@@ -1,8 +1,8 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
+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.
 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 f38526950..73af83f7a 100644
--- a/src/Rewriter/Language/IdentifiersGenerateProofs.v
+++ b/src/Rewriter/Language/IdentifiersGenerateProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import MSetPositive.
+From Coq 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 8884b170b..5fd5aa29c 100644
--- a/src/Rewriter/Language/IdentifiersLibrary.v
+++ b/src/Rewriter/Language/IdentifiersLibrary.v
@@ -1,9 +1,9 @@
-Require Import Coq.Bool.Bool.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
+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.
 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 8ea4cb718..c763cb1c0 100644
--- a/src/Rewriter/Language/IdentifiersLibraryProofs.v
+++ b/src/Rewriter/Language/IdentifiersLibraryProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import MSetPositive.
+From Coq 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 8d8f8c972..9d81f58d8 100644
--- a/src/Rewriter/Language/Language.v
+++ b/src/Rewriter/Language/Language.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+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.
 Require Import Rewriter.Language.PreCommon.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.ListUtil.
diff --git a/src/Rewriter/Language/PreLemmas.v b/src/Rewriter/Language/PreLemmas.v
index 0c2cee826..4a82a4aaf 100644
--- a/src/Rewriter/Language/PreLemmas.v
+++ b/src/Rewriter/Language/PreLemmas.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq 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 9b2711542..e97ea6b7a 100644
--- a/src/Rewriter/Language/Reify.v
+++ b/src/Rewriter/Language/Reify.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+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.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Printf.
 Require Import Rewriter.Language.PreCommon.
diff --git a/src/Rewriter/Language/UnderLetsProofs.v b/src/Rewriter/Language/UnderLetsProofs.v
index 4673650e8..15dcda956 100644
--- a/src/Rewriter/Language/UnderLetsProofs.v
+++ b/src/Rewriter/Language/UnderLetsProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import SetoidList.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
diff --git a/src/Rewriter/Language/Wf.v b/src/Rewriter/Language/Wf.v
index b5f7503c2..5a092ca58 100644
--- a/src/Rewriter/Language/Wf.v
+++ b/src/Rewriter/Language/Wf.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.micromega.Lia.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relations.
+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.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Util.Tactics.BreakMatch.
diff --git a/src/Rewriter/Rewriter/AllTactics.v b/src/Rewriter/Rewriter/AllTactics.v
index 22e4d621e..eaa801ddc 100644
--- a/src/Rewriter/Rewriter/AllTactics.v
+++ b/src/Rewriter/Rewriter/AllTactics.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms.
+From Coq 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 4792d6750..d142cf889 100644
--- a/src/Rewriter/Rewriter/Examples.v
+++ b/src/Rewriter/Rewriter/Examples.v
@@ -1,7 +1,7 @@
 (** * Examples of Using the Rewriter *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
+From Coq 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 ea256a975..519251f9d 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
@@ -1,10 +1,10 @@
-Require Import Coq.QArith.QArith.
-Require Import Coq.Structures.Orders.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Sorting.Mergesort.
-Require Export Coq.Lists.List.
-Require Export Coq.ZArith.ZArith.
+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.
 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 b94c517d4..ff6da5043 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
@@ -1,10 +1,10 @@
-Require Import Coq.Strings.String.
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
+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.
 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 c44b08855..28aa7d58b 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq 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 f67aeb246..dd6f4e22e 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
@@ -1,10 +1,10 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+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.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Import Rewriter.Util.plugins.RewriterBuild.
@@ -99,7 +99,7 @@ Local Instance Z_prod_has_compress : Sample.has_compress (Z * Z) Z := size_of_ar
 Local Instance Z_prod_has_make : Sample.has_make (Z * Z) Z := { make_T := invert_size_of_arg_dumb ; make_T_correct := invert_size_of_arg_dumb_correct }.
 
 Module Import instances.
-  Import Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax.
+  Import QArith Qround Qabs Qminmax.
   Import Sample.
   Local Open Scope Z_scope.
   Local Set Warnings Append "-ambiguous-paths".
@@ -421,7 +421,7 @@ Ltac describe_goal nm :=
 
 Ltac do_coq_rewrite _ := rewrite -> !Z.add_0_r.
 
-Require Import Coq.ssr.ssreflect.
+From Coq 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 00fca2690..7df429969 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 *)
-Require Import Coq.Strings.String.
-Require Import Coq.Structures.Orders.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Sorting.Mergesort.
-Require Import Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax.
-Require Import Coq.NArith.NArith.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Lists.List.
+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.
 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 c94889b9c..b91c6a68d 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
@@ -1,10 +1,10 @@
-Require Import Coq.QArith.QArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Export Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Strings.String.
+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.
 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 c8d8189cd..5c72d4fea 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
@@ -1,10 +1,10 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
-Require Import Coq.Strings.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 Coq 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 99e25712d..e4afe7b0f 100644
--- a/src/Rewriter/Rewriter/Examples/PrefixSums.v
+++ b/src/Rewriter/Rewriter/Examples/PrefixSums.v
@@ -1,8 +1,8 @@
 (** * Examples of Using the Rewriter *)
-Require Import Coq.micromega.Lia.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
+From Coq Require Import Lia.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq 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 6f95a026f..b225f6720 100644
--- a/src/Rewriter/Rewriter/InterpProofs.v
+++ b/src/Rewriter/Rewriter/InterpProofs.v
@@ -1,10 +1,10 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+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.
 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 492ee6051..d02a00991 100644
--- a/src/Rewriter/Rewriter/ProofsCommon.v
+++ b/src/Rewriter/Rewriter/ProofsCommon.v
@@ -1,11 +1,11 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Program.Tactics.
+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.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
index 01cd01529..8e136624d 100644
--- a/src/Rewriter/Rewriter/ProofsCommonTactics.v
+++ b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -1,10 +1,10 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+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.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
diff --git a/src/Rewriter/Rewriter/Reify.v b/src/Rewriter/Rewriter/Reify.v
index 5dc889f46..52ae672e2 100644
--- a/src/Rewriter/Rewriter/Reify.v
+++ b/src/Rewriter/Rewriter/Reify.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq 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 890ee20aa..53219033a 100644
--- a/src/Rewriter/Rewriter/Rewriter.v
+++ b/src/Rewriter/Rewriter/Rewriter.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq 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 31e72a22c..4cf6d558b 100644
--- a/src/Rewriter/Rewriter/Wf.v
+++ b/src/Rewriter/Rewriter/Wf.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+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.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.
diff --git a/src/Rewriter/Util/Bool.v b/src/Rewriter/Util/Bool.v
index 70a5e8222..97e25cc27 100644
--- a/src/Rewriter/Util/Bool.v
+++ b/src/Rewriter/Util/Bool.v
@@ -1,6 +1,6 @@
 (*** Boolean Utility Lemmas and Databases *)
-Require Import Coq.Bool.Bool.
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Bool.
+From Coq 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 217b512b0..122d8632b 100644
--- a/src/Rewriter/Util/Bool/Equality.v
+++ b/src/Rewriter/Util/Bool/Equality.v
@@ -1,3 +1,3 @@
-Require Import Coq.Bool.Bool.
+From Coq Require Import Bool.
 
 Scheme Equality for bool.
diff --git a/src/Rewriter/Util/Bool/Reflect.v b/src/Rewriter/Util/Bool/Reflect.v
index ac807ff4a..6dd39dbd1 100644
--- a/src/Rewriter/Util/Bool/Reflect.v
+++ b/src/Rewriter/Util/Bool/Reflect.v
@@ -1,12 +1,12 @@
 (** * Some lemmas about [Bool.reflect] *)
-Require Import Coq.Classes.CMorphisms.
-Require Import Coq.Strings.String.
-Require Import Coq.Strings.Ascii.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Arith.Arith.
-Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith_dec.
-Require Import Coq.NArith.BinNat.
+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.
 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 875934778..4032101f5 100644
--- a/src/Rewriter/Util/Decidable.v
+++ b/src/Rewriter/Util/Decidable.v
@@ -1,12 +1,12 @@
 (** Typeclass for decidable propositions *)
 
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Coq.Lists.List.
+From Coq Require Import Eqdep_dec.
+From Coq Require Import List.
 Require Import Rewriter.Util.FixCoqMistakes.
 Require Import Rewriter.Util.Sigma.
 Require Import Rewriter.Util.HProp.
-Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith_dec.
-Require Import Coq.NArith.BinNat.
+From Coq Require Import BinInt ZArith_dec.
+From Coq Require Import BinNat.
 
 Local Open Scope type_scope.
 
diff --git a/src/Rewriter/Util/Equality.v b/src/Rewriter/Util/Equality.v
index 5a32e747a..780cd0e75 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. *)
-Require Import Coq.Classes.Morphisms.
+From Coq 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 b61c1fec1..fb0e41425 100644
--- a/src/Rewriter/Util/FMapPositive/Equality.v
+++ b/src/Rewriter/Util/FMapPositive/Equality.v
@@ -1,4 +1,4 @@
-Require Import Coq.FSets.FMapPositive.
+From Coq 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 eb2001133..8a3a94313 100644
--- a/src/Rewriter/Util/FixCoqMistakes.v
+++ b/src/Rewriter/Util/FixCoqMistakes.v
@@ -1,5 +1,5 @@
 (** * Fixes *)
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Morphisms.
 Require Export Rewriter.Util.GlobalSettings.
 
 (** Coq is poorly designed in some ways.  We fix some of these issues
diff --git a/src/Rewriter/Util/IffT.v b/src/Rewriter/Util/IffT.v
index f4eaa9d53..911b204a9 100644
--- a/src/Rewriter/Util/IffT.v
+++ b/src/Rewriter/Util/IffT.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.RelationClasses.
+From Coq 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 8fdf885d2..cb7ae3a98 100644
--- a/src/Rewriter/Util/LetIn.v
+++ b/src/Rewriter/Util/LetIn.v
@@ -1,5 +1,5 @@
 Require Import Rewriter.Util.FixCoqMistakes.
-Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
+From Coq 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 c25893a19..22f9f9807 100644
--- a/src/Rewriter/Util/ListUtil.v
+++ b/src/Rewriter/Util/ListUtil.v
@@ -1,10 +1,10 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Arith.Peano_dec.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Classes.Morphisms.
+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.
 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.
 
-Require Import Coq.Lists.SetoidList.
+From Coq 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 1babb4a8d..8f8004eef 100644
--- a/src/Rewriter/Util/ListUtil/Forall.v
+++ b/src/Rewriter/Util/ListUtil/Forall.v
@@ -1,6 +1,6 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.List.
+From Coq Require Import Lia.
+From Coq Require Import Morphisms.
+From Coq 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 2cdeba922..62a2e70e2 100644
--- a/src/Rewriter/Util/ListUtil/SetoidList.v
+++ b/src/Rewriter/Util/ListUtil/SetoidList.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import List.
+From Coq Require Import Setoid.
+From Coq 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 0a86c218b..fa41d2993 100644
--- a/src/Rewriter/Util/Logic/ExistsEqAnd.v
+++ b/src/Rewriter/Util/Logic/ExistsEqAnd.v
@@ -1,4 +1,4 @@
-Require Import Coq.Setoids.Setoid.
+From Coq 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 32629ae7a..55f791112 100644
--- a/src/Rewriter/Util/MSetPositive/Equality.v
+++ b/src/Rewriter/Util/MSetPositive/Equality.v
@@ -1,4 +1,4 @@
-Require Import Coq.MSets.MSetPositive.
+From Coq 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 259e3334a..56dfc182c 100644
--- a/src/Rewriter/Util/MSetPositive/Facts.v
+++ b/src/Rewriter/Util/MSetPositive/Facts.v
@@ -1,9 +1,9 @@
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.List.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.MSets.MSetFacts.
+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.
 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 4c1c1311d..f0c6ba360 100644
--- a/src/Rewriter/Util/NatUtil.v
+++ b/src/Rewriter/Util/NatUtil.v
@@ -1,9 +1,9 @@
-Require Coq.Logic.Eqdep_dec.
-Require Import Coq.NArith.NArith.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
-Require Import Coq.micromega.Lia.
+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.
 Import Nat.
 
 Scheme Equality for nat.
diff --git a/src/Rewriter/Util/Option.v b/src/Rewriter/Util/Option.v
index dc8ec467c..fc70d67b6 100644
--- a/src/Rewriter/Util/Option.v
+++ b/src/Rewriter/Util/Option.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+From Coq Require Import Morphisms.
+From Coq 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 c6a452df2..a2b34589f 100644
--- a/src/Rewriter/Util/OptionList.v
+++ b/src/Rewriter/Util/OptionList.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq 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 c9ce5f94b..a33b1906e 100644
--- a/src/Rewriter/Util/Pointed.v
+++ b/src/Rewriter/Util/Pointed.v
@@ -1,4 +1,4 @@
-Require Import Coq.Numbers.BinNums.
+From Coq Require Import BinNums.
 
 Local Generalizable All Variables.
 
diff --git a/src/Rewriter/Util/PrimitiveHList.v b/src/Rewriter/Util/PrimitiveHList.v
index 609fb71e6..1a1ffba81 100644
--- a/src/Rewriter/Util/PrimitiveHList.v
+++ b/src/Rewriter/Util/PrimitiveHList.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq 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 94efa6426..ab3f6d812 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. *)
-Require Import Coq.Classes.Morphisms.
+From Coq 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 c8703f30d..81010e633 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. *)
-Require Import Coq.Classes.Morphisms.
+From Coq 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 934a52f8f..d8f7b1005 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. *)
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Bool.Bool.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq 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 bc3bacb90..0d72483de 100644
--- a/src/Rewriter/Util/Sigma/Related.v
+++ b/src/Rewriter/Util/Sigma/Related.v
@@ -1,6 +1,6 @@
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+From Coq Require Import RelationClasses.
+From Coq Require Import Morphisms.
+From Coq 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 e44c75ca7..b32a84781 100644
--- a/src/Rewriter/Util/Strings/Ascii.v
+++ b/src/Rewriter/Util/Strings/Ascii.v
@@ -1,5 +1,5 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.Strings.Ascii.
+From Coq Require Import NArith.
+From Coq 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 868242fae..af6a71dd6 100644
--- a/src/Rewriter/Util/Strings/Decimal.v
+++ b/src/Rewriter/Util/Strings/Decimal.v
@@ -1,8 +1,8 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String.
-Require Import Coq.Numbers.BinNums.
-Require Import Coq.Numbers.DecimalString.
-Require Coq.Numbers.DecimalN.
-Require Coq.Numbers.DecimalZ.
+From Coq Require Import Ascii String.
+From Coq Require Import BinNums.
+From Coq Require Import DecimalString.
+From Coq Require DecimalN.
+From Coq 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 f5956ceec..1adf06c20 100644
--- a/src/Rewriter/Util/Strings/Parse/Common.v
+++ b/src/Rewriter/Util/Strings/Parse/Common.v
@@ -1,4 +1,4 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List.
+From Coq 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 d59075b33..a5124e839 100644
--- a/src/Rewriter/Util/Strings/ParseArithmetic.v
+++ b/src/Rewriter/Util/Strings/ParseArithmetic.v
@@ -1,11 +1,11 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List.
-Require Import Coq.Numbers.BinNums.
-Require Import Coq.QArith.QArith.
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import Ascii String List.
+From Coq Require Import BinNums.
+From Coq Require Import QArith.
+From Coq Require Import BinInt.
 Require Import Rewriter.Util.Option.
-Require Coq.Strings.BinaryString.
-Require Coq.Strings.OctalString.
-Require Coq.Strings.HexString.
+From Coq Require BinaryString.
+From Coq Require OctalString.
+From Coq 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 1b6f0030d..d9da2bb78 100644
--- a/src/Rewriter/Util/Strings/String.v
+++ b/src/Rewriter/Util/Strings/String.v
@@ -1,7 +1,7 @@
-Require Import Coq.Arith.PeanoNat.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Strings.String.
-Require Import Coq.Strings.Ascii.
+From Coq Require Import PeanoNat.
+From Coq Require Import Lia.
+From Coq Require Import String.
+From Coq 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 3093beb4f..086b8e10a 100644
--- a/src/Rewriter/Util/Sum.v
+++ b/src/Rewriter/Util/Sum.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+From Coq Require Import Morphisms.
+From Coq Require Import Relation_Definitions.
 Require Import Rewriter.Util.Decidable.
 Require Import Rewriter.Util.Tactics.DestructHead.
 Require Import Rewriter.Util.Tactics.SetoidSubst.