diff --git a/PerformanceExperiments/Harness.v b/PerformanceExperiments/Harness.v
index 690baa6cfe..7d2300a430 100644
--- a/PerformanceExperiments/Harness.v
+++ b/PerformanceExperiments/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.
 Require Import PerformanceExperiments.Sandbox.
 Export ListNotations.
 
diff --git a/PerformanceExperiments/LetIn.v b/PerformanceExperiments/LetIn.v
index 7ba6481642..f82bec3172 100644
--- a/PerformanceExperiments/LetIn.v
+++ b/PerformanceExperiments/LetIn.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
 
 Reserved Notation "'dlet' x .. y := v 'in' f"
          (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
diff --git a/PerformanceExperiments/ListRectInstances.v b/PerformanceExperiments/ListRectInstances.v
index c44b08855a..28aa7d58b7 100644
--- a/PerformanceExperiments/ListRectInstances.v
+++ b/PerformanceExperiments/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/PerformanceExperiments/PrimitiveProd.v b/PerformanceExperiments/PrimitiveProd.v
index a258f85d3c..8e099a6e9a 100644
--- a/PerformanceExperiments/PrimitiveProd.v
+++ b/PerformanceExperiments/PrimitiveProd.v
@@ -1,5 +1,5 @@
 (** * Define a primitive pairing type *)
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Morphisms.
 
 Local Set Primitive Projections.
 
diff --git a/PerformanceExperiments/Reify/BenchmarkExtraUtil.v b/PerformanceExperiments/Reify/BenchmarkExtraUtil.v
index b334cb785f..ad018c3c80 100644
--- a/PerformanceExperiments/Reify/BenchmarkExtraUtil.v
+++ b/PerformanceExperiments/Reify/BenchmarkExtraUtil.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.NArith.NArith.
+From Coq Require Import List.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Sandbox.
 Require Import Reify.ReifyCommon.
 Require Import Reify.PHOASUtil.
diff --git a/PerformanceExperiments/Reify/BenchmarkUtil.v b/PerformanceExperiments/Reify/BenchmarkUtil.v
index e0597f1a55..6e0c017d7c 100644
--- a/PerformanceExperiments/Reify/BenchmarkUtil.v
+++ b/PerformanceExperiments/Reify/BenchmarkUtil.v
@@ -1,5 +1,5 @@
 (** * Various utilities for benchmarking *)
-Require Import Coq.NArith.NArith. (* for Pos.iter_op and Z.of_nat *)
+From Coq Require Import NArith. (* for Pos.iter_op and Z.of_nat *)
 Require Import Reify.Common.
 Require Reify.PHOAS.
 Require Import Reify.PHOASUtil.
diff --git a/PerformanceExperiments/Reify/CanonicalStructures.v b/PerformanceExperiments/Reify/CanonicalStructures.v
index 19acbd1d72..f24cbf61fa 100644
--- a/PerformanceExperiments/Reify/CanonicalStructures.v
+++ b/PerformanceExperiments/Reify/CanonicalStructures.v
@@ -1,7 +1,7 @@
 (** * Canonical-structure based reification *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.Lists.List.
-Require Import Coq.NArith.NArith.
+From Coq Require Import List.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 Require Import Reify.CanonicalStructuresReifyCommon.
diff --git a/PerformanceExperiments/Reify/Ltac2.v b/PerformanceExperiments/Reify/Ltac2.v
index eb185ea111..b76324405e 100644
--- a/PerformanceExperiments/Reify/Ltac2.v
+++ b/PerformanceExperiments/Reify/Ltac2.v
@@ -1,6 +1,6 @@
 (** * Reification by Ltac2 *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.Ltac2Reify.
 Require Import Reify.BenchmarkExtraUtil.
diff --git a/PerformanceExperiments/Reify/LtacVariants.v b/PerformanceExperiments/Reify/LtacVariants.v
index 01d8e03857..cc01472da5 100644
--- a/PerformanceExperiments/Reify/LtacVariants.v
+++ b/PerformanceExperiments/Reify/LtacVariants.v
@@ -1,5 +1,5 @@
 (** * Ltac-based reification, using uncurrying to reucurse under binders *)
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 Require
diff --git a/PerformanceExperiments/Reify/OCaml.v b/PerformanceExperiments/Reify/OCaml.v
index 09f00cf965..0428f7e512 100644
--- a/PerformanceExperiments/Reify/OCaml.v
+++ b/PerformanceExperiments/Reify/OCaml.v
@@ -1,7 +1,7 @@
 (** * Reification in OCaml *)
 Require Import Reify.ReifyCommon.
 Require Import Reify.OCamlReify.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 (** See [OCamlReify.v] and [reify_plugin.{ml4,mlg}] for the implementation code. *)
diff --git a/PerformanceExperiments/Reify/Parametricity.v b/PerformanceExperiments/Reify/Parametricity.v
index e40d1278f3..a55cb39171 100644
--- a/PerformanceExperiments/Reify/Parametricity.v
+++ b/PerformanceExperiments/Reify/Parametricity.v
@@ -1,6 +1,6 @@
 (** * Reification by parametricity *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.ParametricityCommon.
 Require Import Reify.BenchmarkExtraUtil.
diff --git a/PerformanceExperiments/Reify/QuoteFlat.v b/PerformanceExperiments/Reify/QuoteFlat.v
index d583d1b013..b989122d46 100644
--- a/PerformanceExperiments/Reify/QuoteFlat.v
+++ b/PerformanceExperiments/Reify/QuoteFlat.v
@@ -1,7 +1,7 @@
 (** * Reification by the quote plugin *)
-Require Import Coq.quote.Quote.
+From Coq Require Import Quote.
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 
diff --git a/PerformanceExperiments/Reify/TypeClasses.v b/PerformanceExperiments/Reify/TypeClasses.v
index 9f3109267d..92c5e3d82a 100644
--- a/PerformanceExperiments/Reify/TypeClasses.v
+++ b/PerformanceExperiments/Reify/TypeClasses.v
@@ -1,6 +1,6 @@
 (** * Typeclass-based reification *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 
diff --git a/PerformanceExperiments/Sample.v b/PerformanceExperiments/Sample.v
index f13facb07c..a5c4a8194a 100644
--- a/PerformanceExperiments/Sample.v
+++ b/PerformanceExperiments/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 PerformanceExperiments.LetIn.
 Import ListNotations.
 Local Open Scope list_scope.
diff --git a/PerformanceExperiments/n_polymorphic_universes.v b/PerformanceExperiments/n_polymorphic_universes.v
index 59c710cf26..9c590ed853 100644
--- a/PerformanceExperiments/n_polymorphic_universes.v
+++ b/PerformanceExperiments/n_polymorphic_universes.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import PerformanceExperiments.Harness.
 Global Open Scope Z_scope.
 Set Universe Polymorphism.
diff --git a/PerformanceExperiments/rewrite_lift_lets_map.v b/PerformanceExperiments/rewrite_lift_lets_map.v
index ae417f6057..bbfba11ad5 100644
--- a/PerformanceExperiments/rewrite_lift_lets_map.v
+++ b/PerformanceExperiments/rewrite_lift_lets_map.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Require Export PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances.
diff --git a/PerformanceExperiments/rewrite_plus_0_tree.v b/PerformanceExperiments/rewrite_plus_0_tree.v
index dac280de66..58edc0353b 100644
--- a/PerformanceExperiments/rewrite_plus_0_tree.v
+++ b/PerformanceExperiments/rewrite_plus_0_tree.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Import ListNotations.
@@ -91,7 +91,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".
@@ -346,7 +346,7 @@ Hint Rewrite Z.add_0_r : mydb.
 
 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/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v b/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v
index ccf833aaf5..b44abee14f 100644
--- a/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v
+++ b/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v
@@ -20,7 +20,7 @@ Ltac do_rewrite_ques := try rewrite ?fg.
 Ltac do_rewrite_bang_evar := try rewrite !(fg _).
 Ltac do_rewrite_once_evar := try rewrite (fg _).
 Ltac do_rewrite_ques_evar := try rewrite ?(fg _).
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 Ltac do_ssr_rewrite_bang := try rewrite !fg.
 Ltac do_ssr_rewrite_once := try rewrite fg.
 Ltac do_ssr_rewrite_ques := try rewrite ?fg.
diff --git a/PerformanceExperiments/rewrite_repeated_app_common.v b/PerformanceExperiments/rewrite_repeated_app_common.v
index e82bd7bbfa..023934c2c0 100644
--- a/PerformanceExperiments/rewrite_repeated_app_common.v
+++ b/PerformanceExperiments/rewrite_repeated_app_common.v
@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+From Coq Require Import ZArith.
+From Coq Require Import Setoid Morphisms.
 Local Open Scope core_scope.
 Axiom f : nat -> nat.
 Axiom g : nat -> nat.
diff --git a/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v b/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v
index e0bd0371ae..80bc71a916 100644
--- a/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v
+++ b/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v
@@ -1,4 +1,4 @@
-Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+From Coq Require Import Setoid Morphisms.
 Require Export PerformanceExperiments.rewrite_repeated_app_common.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Constr.
diff --git a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v
index d8bea55310..2444b8b449 100644
--- a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v
+++ b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v
@@ -12,7 +12,7 @@ Definition args_of_size (s : size) : list nat
      | VerySlow => []
      end.
 
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 
 Ltac do_rewrite := rewrite !fg.
 
diff --git a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v
index f9ea9747a0..919fbe09ad 100644
--- a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v
+++ b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v
@@ -1,4 +1,4 @@
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 Require Import PerformanceExperiments.Harness.
 Require Export PerformanceExperiments.rewrite_repeated_app_common.
 
@@ -12,7 +12,7 @@ Definition args_of_size (s : size) : list nat
      | VerySlow => []
      end.
 
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 Ltac do_ssr_rewrite_bang := try rewrite !f'g'.
 Ltac do_ssr_rewrite_once := try rewrite f'g'.
 Ltac do_ssr_rewrite_ques := try rewrite ?f'g'.
diff --git a/PerformanceExperiments/rewrite_under_binders_common.v b/PerformanceExperiments/rewrite_under_binders_common.v
index a0d5b3a222..0f2986b6cf 100644
--- a/PerformanceExperiments/rewrite_under_binders_common.v
+++ b/PerformanceExperiments/rewrite_under_binders_common.v
@@ -1,6 +1,6 @@
 (** * performance of rewrite/rewrite_strat under binders *)
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
 
 Module Type LetInT.
   Parameter Let_In : forall {A P} (x : A) (f : forall a : A, P a), P x.
diff --git a/PerformanceExperiments/rewrite_under_lets_plus_0.v b/PerformanceExperiments/rewrite_under_lets_plus_0.v
index 081c6a3509..cdabae2867 100644
--- a/PerformanceExperiments/rewrite_under_lets_plus_0.v
+++ b/PerformanceExperiments/rewrite_under_lets_plus_0.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Require Export PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances.
diff --git a/PerformanceExperiments/sieve_of_eratosthenes.v b/PerformanceExperiments/sieve_of_eratosthenes.v
index 2ebae78095..f873c5f62b 100644
--- a/PerformanceExperiments/sieve_of_eratosthenes.v
+++ b/PerformanceExperiments/sieve_of_eratosthenes.v
@@ -1,9 +1,9 @@
-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.
+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.
 Require Import PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Import ListNotations.
diff --git a/src/Nia.v b/src/Nia.v
index 2bfa681553..1bf07d051b 100644
--- a/src/Nia.v
+++ b/src/Nia.v
@@ -1,6 +1,6 @@
 (* -*- coqchk-prog-args: ("-bytecode-compiler" "yes") -*- *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
 Open Scope Z_scope.
 
 (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
diff --git a/src/fiat_crypto_via_setoid_rewrite_standalone.v b/src/fiat_crypto_via_setoid_rewrite_standalone.v
index 0e6a8bff0e..7a1f078fbf 100644
--- a/src/fiat_crypto_via_setoid_rewrite_standalone.v
+++ b/src/fiat_crypto_via_setoid_rewrite_standalone.v
@@ -1,8 +1,8 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import QArith_base Qreduction Qround.
 Import List.ListNotations.
 Local Open Scope Z_scope.
 Local Open Scope list_scope.
diff --git a/src/n_polymorphic_universes.v b/src/n_polymorphic_universes.v
index 3471f0966a..cea9414e14 100644
--- a/src/n_polymorphic_universes.v
+++ b/src/n_polymorphic_universes.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Local Open Scope Z_scope.
 Set Universe Polymorphism.
 Record prod A B := pair { fst : A ; snd : B }.