diff --git a/src/Common.v b/src/Common.v
index 758fac87..44107306 100644
--- a/src/Common.v
+++ b/src/Common.v
@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith Coq.Lists.SetoidList.
+From Coq Require Import ZArith.ZArith SetoidList.
 Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses
         Coq.Program.Program Coq.Classes.Morphisms.
 Require Export Fiat.Common.Tactics.SplitInContext.
diff --git a/src/Common/Equality.v b/src/Common/Equality.v
index ac949828..75102520 100644
--- a/src/Common/Equality.v
+++ b/src/Common/Equality.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Coq.Lists.SetoidList.
+From Coq Require Import List SetoidList.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.Ascii.
diff --git a/src/Common/List/FlattenList.v b/src/Common/List/FlattenList.v
index 74c46cd3..5165f86b 100644
--- a/src/Common/List/FlattenList.v
+++ b/src/Common/List/FlattenList.v
@@ -1,4 +1,5 @@
-Require Import Coq.Lists.List Coq.Lists.SetoidList Fiat.Common.
+From Coq Require Import List SetoidList.
+Require Import Fiat.Common.
 Require Import Coq.Arith.Arith.
 
 Unset Implicit Arguments.
diff --git a/src/Common/List/ListFacts.v b/src/Common/List/ListFacts.v
index 09c57843..02d4eb95 100644
--- a/src/Common/List/ListFacts.v
+++ b/src/Common/List/ListFacts.v
@@ -1,7 +1,7 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool
-        Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.
+From Coq Require Import List SetoidList Bool.
+Require Import Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.
 
 Unset Implicit Arguments.
 
diff --git a/src/Common/List/PermutationFacts.v b/src/Common/List/PermutationFacts.v
index c4e7f730..357cb15f 100644
--- a/src/Common/List/PermutationFacts.v
+++ b/src/Common/List/PermutationFacts.v
@@ -220,7 +220,7 @@ Proof.
   apply Permutation_length_1 in H; congruence.
 Qed.
 
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 
 Lemma InA_app_swap {A} eqA :
   Equivalence eqA
diff --git a/src/Common/Wf.v b/src/Common/Wf.v
index 9be4543d..0beffb17 100644
--- a/src/Common/Wf.v
+++ b/src/Common/Wf.v
@@ -1,6 +1,9 @@
 (** * Miscellaneous Well-Foundedness Facts *)
-Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import Setoid.
+From Coq.Program Require Import Program Wf.
+From Coq Require Import Wf_nat Morphisms.
+From Coq.Init Require Import Wf.
+From Coq Require Import SetoidList.
 Require Import Coq.Arith.PeanoNat.
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 
diff --git a/src/Computation/Decidable.v b/src/Computation/Decidable.v
index 027d6d4c..9bfaf7d5 100644
--- a/src/Computation/Decidable.v
+++ b/src/Computation/Decidable.v
@@ -139,7 +139,7 @@ Global Program Instance bool_eq_Decidable {n m : bool} : Decidable (n = m) := {
 Obligation 1. t' eqb_true_iff. Qed.
 
 Require Import Coq.Strings.Ascii.
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 
 Global Program Instance ascii_eq_Decidable {n m : Ascii.ascii} :
   Decidable (n = m) := {