diff --git a/lf-current/Extraction.v b/lf-current/Extraction.v
index 2d1d5d91c..bed0b8bed 100644
--- a/lf-current/Extraction.v
+++ b/lf-current/Extraction.v
@@ -10,15 +10,15 @@
     OCaml (the most mature), Haskell (mostly works), and Scheme (a bit
     out of date). *)
 
-Require Coq.extraction.Extraction.
+From Coq Require Extraction.
 Extraction Language OCaml.
 
 (** Now we load up the Coq environment with some definitions, either
     directly or by importing them from other modules. *)
 
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import EqNat.
 From LF Require Import ImpCEvalFun.
 
 (** Finally, we tell Coq the name of a definition to extract and the
diff --git a/lf-current/Imp.v b/lf-current/Imp.v
index d24ce1f8a..cf8b89752 100644
--- a/lf-current/Imp.v
+++ b/lf-current/Imp.v
@@ -22,12 +22,12 @@
     reasoning about imperative programs. *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Arith.
+From Coq Require Import EqNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 From Coq Require Import Strings.String.
 From LF Require Import Maps.
 Set Default Goal Selector "!".
diff --git a/lf-current/ImpCEvalFun.v b/lf-current/ImpCEvalFun.v
index 1b7a5cb36..5445ee7a4 100644
--- a/lf-current/ImpCEvalFun.v
+++ b/lf-current/ImpCEvalFun.v
@@ -11,10 +11,10 @@
 (** * A Broken Evaluator *)
 
 From Coq Require Import Lia.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.PeanoNat.
+From Coq Require Import Arith.
+From Coq Require Import PeanoNat.
 Import Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import EqNat.
 From LF Require Import Imp Maps.
 
 (** Here was our first try at an evaluation function for commands,
diff --git a/lf-current/ImpParser.v b/lf-current/ImpParser.v
index 16b801dc5..d3ab47cfa 100644
--- a/lf-current/ImpParser.v
+++ b/lf-current/ImpParser.v
@@ -20,10 +20,10 @@
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From Coq Require Import Strings.String.
 From Coq Require Import Strings.Ascii.
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import EqNat.
+From Coq Require Import List. Import ListNotations.
 From LF Require Import Maps Imp.
 
 (* ################################################################# *)
diff --git a/lf-current/Maps.v b/lf-current/Maps.v
index 451a13791..91d4fc724 100644
--- a/lf-current/Maps.v
+++ b/lf-current/Maps.v
@@ -29,11 +29,11 @@
     own definitions and theorems the same as their counterparts in the
     standard library, wherever they overlap. *)
 
-From Coq Require Import Arith.Arith.
-From Coq Require Import Bool.Bool.
-Require Export Coq.Strings.String.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import Arith.
+From Coq Require Import Bool.
+From Coq Require Export String.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 Set Default Goal Selector "!".
 
diff --git a/lf-current/imp.ml b/lf-current/imp.ml
index 242b11e1e..36ef7fe0c 100644
--- a/lf-current/imp.ml
+++ b/lf-current/imp.ml
@@ -12,12 +12,9 @@ let rec app l m =
   | [] -> m
   | a :: l1 -> a :: (app l1 m)
 
-module Coq__1 = struct
- (** val add : int -> int -> int **)
+(** val add : int -> int -> int **)
 
- let rec add = ( + )
-end
-include Coq__1
+let rec add = ( + )
 
 (** val mul : int -> int -> int **)
 
@@ -133,6 +130,22 @@ type n =
 | Npos of positive
 
 module Pos =
+ struct
+  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
+
+  let rec iter_op op p a =
+    match p with
+    | XI p0 -> op a (iter_op op p0 (op a a))
+    | XO p0 -> iter_op op p0 (op a a)
+    | XH -> a
+
+  (** val to_nat : positive -> int **)
+
+  let to_nat x =
+    iter_op add x ((fun x -> x + 1) 0)
+ end
+
+module Coq_Pos =
  struct
   (** val succ : positive -> positive **)
 
@@ -187,19 +200,6 @@ module Pos =
     | XI p -> add y (XO (mul p y))
     | XO p -> XO (mul p y)
     | XH -> y
-
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
-
-  let rec iter_op op p a =
-    match p with
-    | XI p0 -> op a (iter_op op p0 (op a a))
-    | XO p0 -> iter_op op p0 (op a a)
-    | XH -> a
-
-  (** val to_nat : positive -> int **)
-
-  let to_nat x =
-    iter_op Coq__1.add x ((fun x -> x + 1) 0)
  end
 
 module N =
@@ -211,7 +211,7 @@ module N =
     | N0 -> m
     | Npos p -> (match m with
                  | N0 -> n0
-                 | Npos q -> Npos (Pos.add p q))
+                 | Npos q -> Npos (Coq_Pos.add p q))
 
   (** val mul : n -> n -> n **)
 
@@ -220,7 +220,7 @@ module N =
     | N0 -> N0
     | Npos p -> (match m with
                  | N0 -> N0
-                 | Npos q -> Npos (Pos.mul p q))
+                 | Npos q -> Npos (Coq_Pos.mul p q))
 
   (** val to_nat : n -> int **)
 
@@ -229,18 +229,18 @@ module N =
   | Npos p -> Pos.to_nat p
  end
 
-(** val rev : 'a1 list -> 'a1 list **)
-
-let rec rev = function
-| [] -> []
-| x :: l' -> app (rev l') (x :: [])
-
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
 let rec map f = function
 | [] -> []
 | a :: t -> (f a) :: (map f t)
 
+(** val rev : 'a1 list -> 'a1 list **)
+
+let rec rev = function
+| [] -> []
+| x :: l' -> app (rev l') (x :: [])
+
 (** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
 
 let rec fold_left f l a0 =
diff --git a/lf-current/imp.mli b/lf-current/imp.mli
index 76d67bacf..95ed27189 100644
--- a/lf-current/imp.mli
+++ b/lf-current/imp.mli
@@ -36,6 +36,13 @@ type n =
 | Npos of positive
 
 module Pos :
+ sig
+  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
+
+  val to_nat : positive -> int
+ end
+
+module Coq_Pos :
  sig
   val succ : positive -> positive
 
@@ -44,10 +51,6 @@ module Pos :
   val add_carry : positive -> positive -> positive
 
   val mul : positive -> positive -> positive
-
-  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
-
-  val to_nat : positive -> int
  end
 
 module N :
@@ -59,10 +62,10 @@ module N :
   val to_nat : n -> int
  end
 
-val rev : 'a1 list -> 'a1 list
-
 val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
 
+val rev : 'a1 list -> 'a1 list
+
 val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
 
 val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
diff --git a/plf-current/Equiv.v b/plf-current/Equiv.v
index a26b3116a..c9ba6fb73 100644
--- a/plf-current/Equiv.v
+++ b/plf-current/Equiv.v
@@ -2,14 +2,14 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import PeanoNat. Import Nat.
+From Coq Require Import EqNat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
-From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import List. Import ListNotations.
+From Coq Require Import FunctionalExtensionality.
 From PLF Require Export Imp.
 Set Default Goal Selector "!".
 
diff --git a/plf-current/Hoare.v b/plf-current/Hoare.v
index 2b28a3ba6..18ae74734 100644
--- a/plf-current/Hoare.v
+++ b/plf-current/Hoare.v
@@ -2,10 +2,10 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
 From PLF Require Export Imp.
 Set Default Goal Selector "!".
diff --git a/plf-current/Hoare2.v b/plf-current/Hoare2.v
index 4c2da0fd7..dc32662e1 100644
--- a/plf-current/Hoare2.v
+++ b/plf-current/Hoare2.v
@@ -4,10 +4,10 @@ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 Set Warnings "-intuition-auto-with-star".
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
 From PLF Require Export Imp.
 From PLF Require Import Hoare.
diff --git a/plf-current/Imp.v b/plf-current/Imp.v
index 9038b25ed..49b4765cb 100644
--- a/plf-current/Imp.v
+++ b/plf-current/Imp.v
@@ -22,12 +22,12 @@
     reasoning about imperative programs. *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Arith.
+From Coq Require Import EqNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
 Set Default Goal Selector "!".
diff --git a/plf-current/LibTactics.v b/plf-current/LibTactics.v
index 503df955c..f92ad22ea 100644
--- a/plf-current/LibTactics.v
+++ b/plf-current/LibTactics.v
@@ -368,7 +368,7 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [Z] type. *)
 
-Require Coq.Numbers.BinNums Coq.ZArith.BinInt.
+From Coq Require BinNums BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -2536,7 +2536,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ================================================================= *)
 (** ** Tactics to Work with Proof Irrelevance *)
 
-Require Import Coq.Logic.ProofIrrelevance.
+From Coq Require Import ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
     unification variable, and is thus a practical way to
@@ -3138,7 +3138,7 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
-Require Import Coq.Program.Equality.
+From Coq.Program Require Import Equality.
 
 Ltac inductions_post :=
   unfold eq' in *.
@@ -3215,8 +3215,8 @@ Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
-Require Import Coq.Arith.Compare_dec.
-Require Import Coq.micromega.Lia.
+From Coq Require Import Compare_dec.
+From Coq Require Import Lia.
 
 Lemma induct_height_max2 : forall n1 n2 : nat,
   exists n, n1 < n /\ n2 < n.
diff --git a/plf-current/Maps.v b/plf-current/Maps.v
index c8f79ecd6..b3755b169 100644
--- a/plf-current/Maps.v
+++ b/plf-current/Maps.v
@@ -29,11 +29,11 @@
     own definitions and theorems the same as their counterparts in the
     standard library, wherever they overlap. *)
 
-From Coq Require Import Arith.Arith.
-From Coq Require Import Bool.Bool.
+From Coq Require Import Arith.
+From Coq Require Import Bool.
 Require Export Coq.Strings.String.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 Set Default Goal Selector "!".
 
diff --git a/plf-current/Norm.v b/plf-current/Norm.v
index d895bd1c6..9a1f001b1 100644
--- a/plf-current/Norm.v
+++ b/plf-current/Norm.v
@@ -1,7 +1,7 @@
 (** * Norm: Normalization of STLC *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Lists.List.
+From Coq Require Import List.
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
diff --git a/plf-current/PE.v b/plf-current/PE.v
index 9b7b20907..d0f0c34f0 100644
--- a/plf-current/PE.v
+++ b/plf-current/PE.v
@@ -35,13 +35,13 @@
     without knowing the initial value of [Y]. *)
 
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 
 From PLF Require Import Smallstep.
diff --git a/plf-current/References.v b/plf-current/References.v
index 8f42e15f8..be290fe0c 100644
--- a/plf-current/References.v
+++ b/plf-current/References.v
@@ -33,12 +33,12 @@ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 Set Warnings "-deprecated-syntactic-definition".
 From Coq Require Import Strings.String.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.PeanoNat.
+From Coq Require Import Arith.
+From Coq Require Import PeanoNat.
 From Coq Require Import Lia.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
-From Coq Require Import Lists.List. Import Datatypes.
+From Coq Require Import List. Import Datatypes.
 Check length.
 
 Import Nat.
diff --git a/plf-current/Smallstep.v b/plf-current/Smallstep.v
index cbb07b784..8273d32ef 100644
--- a/plf-current/Smallstep.v
+++ b/plf-current/Smallstep.v
@@ -1,11 +1,11 @@
 (** * Smallstep: Small-step Operational Semantics *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
 From Coq Require Import Init.Nat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 From PLF Require Import Maps.
 From PLF Require Import Imp.
 Set Default Goal Selector "!".
diff --git a/plf-current/Typechecking.v b/plf-current/Typechecking.v
index 025bb1fe3..78dd019af 100644
--- a/plf-current/Typechecking.v
+++ b/plf-current/Typechecking.v
@@ -18,7 +18,7 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 Set Warnings "-non-recursive".
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
 From PLF Require Import Stlc.
diff --git a/plf-current/Types.v b/plf-current/Types.v
index f4caec44c..66ded50c5 100644
--- a/plf-current/Types.v
+++ b/plf-current/Types.v
@@ -11,7 +11,7 @@
     Coq!). *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
 Set Default Goal Selector "!".
diff --git a/plf-current/UseAuto.v b/plf-current/UseAuto.v
index a47b3c475..6f0f9e5d5 100644
--- a/plf-current/UseAuto.v
+++ b/plf-current/UseAuto.v
@@ -26,7 +26,7 @@
     from the library [LibTactics.v], which is presented in the chapter
     [UseTactics]. *)
 
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
@@ -34,7 +34,7 @@ From PLF Require Import LibTactics.
 From PLF Require Stlc.
 From PLF Require Imp.
 
-From Coq Require Import Lists.List.
+From Coq Require Import List.
 
 
 (* ################################################################# *)
diff --git a/plf-current/UseTactics.v b/plf-current/UseTactics.v
index 07e9ffd14..bac13e6e5 100644
--- a/plf-current/UseTactics.v
+++ b/plf-current/UseTactics.v
@@ -12,7 +12,7 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 
 From PLF Require Maps.
 From PLF Require Stlc.
diff --git a/qc-current/Typeclasses.v b/qc-current/Typeclasses.v
index 659da6758..9ff51f81e 100644
--- a/qc-current/Typeclasses.v
+++ b/qc-current/Typeclasses.v
@@ -1,8 +1,8 @@
 (** * Typeclasses: A Tutorial on Typeclasses in Coq *)
 
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From Coq Require Import Strings.String.
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From Coq Require Import Lia.
 Require Import List. Import ListNotations.
 Local Open Scope string.
diff --git a/slf-current/LibEqual.v b/slf-current/LibEqual.v
index 93d34ee82..73b0384c2 100644
--- a/slf-current/LibEqual.v
+++ b/slf-current/LibEqual.v
@@ -874,7 +874,7 @@ Proof using. introv E. dependent rewrite E. simple~. constructor. Qed.
 (* ################################################################# *)
 (** * John Major's equality *)
 
-Require Import Coq.Logic.JMeq.
+From Coq Require Import JMeq.
 
 (** The module above defines John Major's equality:
 
diff --git a/slf-current/LibInt.v b/slf-current/LibInt.v
index f596618a2..f2c8eaf5d 100644
--- a/slf-current/LibInt.v
+++ b/slf-current/LibInt.v
@@ -8,7 +8,7 @@
 **************************************************************************)
 
 Set Implicit Arguments.
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 From SLF Require Import LibTactics LibLogic LibReflect LibRelation.
 Export LibTacticsCompatibility.
 From SLF Require Export LibNat.
diff --git a/slf-current/LibNat.v b/slf-current/LibNat.v
index 72a01b091..ef00a2a35 100644
--- a/slf-current/LibNat.v
+++ b/slf-current/LibNat.v
@@ -8,7 +8,7 @@
 **************************************************************************)
 
 Set Implicit Arguments.
-Require Export Coq.Arith.Arith Coq.micromega.Lia.
+From Coq Require Export Arith Lia.
 From SLF Require Import LibTactics LibReflect LibBool LibOperation LibRelation LibOrder.
 From SLF Require Export LibOrder.
 Global Close Scope positive_scope.
diff --git a/slf-current/LibTactics.v b/slf-current/LibTactics.v
index 9accb8be4..1d87e1161 100644
--- a/slf-current/LibTactics.v
+++ b/slf-current/LibTactics.v
@@ -379,7 +379,7 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [Z] type. *)
 
-Require Coq.Numbers.BinNums Coq.ZArith.BinInt.
+From Coq Require BinNums BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -2582,7 +2582,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ================================================================= *)
 (** ** Tactics to Work with Proof Irrelevance *)
 
-Require Import Coq.Logic.ProofIrrelevance.
+From Coq Require Import ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
     unification variable, and is thus a practical way to
@@ -3237,7 +3237,7 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
-Require Import Coq.Program.Equality.
+From Coq Require Import Equality.
 
 Ltac inductions_post :=
   unfold eq' in *.
@@ -3314,8 +3314,8 @@ Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
-Require Import Coq.Arith.Compare_dec.
-Require Import Coq.micromega.Lia.
+From Coq Require Import Compare_dec.
+From Coq Require Import Lia.
 
 Lemma induct_height_max2 : forall n1 n2 : nat,
   exists n, n1 < n /\ n2 < n.
diff --git a/vfa-current/Maps.v b/vfa-current/Maps.v
index b326c7388..448479f7b 100644
--- a/vfa-current/Maps.v
+++ b/vfa-current/Maps.v
@@ -6,8 +6,8 @@
     indicate success or failure. We'll use maps in upcoming chapters
     to verify other data structures. *)
 
-From Coq Require Import Bool.Bool.
-From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Bool.
+From Coq Require Import FunctionalExtensionality.
 From VFA Require Import Perm.
 
 (* ################################################################# *)
diff --git a/vfa-current/Perm.v b/vfa-current/Perm.v
index 6f3c3e45b..9dd86bcf5 100644
--- a/vfa-current/Perm.v
+++ b/vfa-current/Perm.v
@@ -30,11 +30,11 @@
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From Coq Require Import Strings.String.  (* for manual grading *)
 From Coq Require Export Bool.Bool.
-From Coq Require Export Arith.Arith.
-From Coq Require Export Arith.PeanoNat.
-From Coq Require Export Arith.EqNat.
+From Coq Require Export Arith.
+From Coq Require Export PeanoNat.
+From Coq Require Export EqNat.
 From Coq Require Export Lia.
-From Coq Require Export Lists.List.
+From Coq Require Export List.
 Export ListNotations.
 From Coq Require Export Permutation.
 
diff --git a/vfa-current/Redblack.v b/vfa-current/Redblack.v
index 020e64bc0..b469fc282 100644
--- a/vfa-current/Redblack.v
+++ b/vfa-current/Redblack.v
@@ -32,7 +32,7 @@
 
 Set Warnings "-undo-batch-mode".
 From Coq Require Import String.
-From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import FunctionalExtensionality.
 From Coq Require Import ZArith.
 From VFA Require Import Perm.
 From VFA Require Import Extract.
diff --git a/vfa-current/SearchTree.v b/vfa-current/SearchTree.v
index f4daff453..a1d289558 100644
--- a/vfa-current/SearchTree.v
+++ b/vfa-current/SearchTree.v
@@ -23,7 +23,7 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From Coq Require Import String.  (* for an example, and manual grading *)
-From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import FunctionalExtensionality.
 From VFA Require Import Perm.
 From VFA Require Import Maps.
 From VFA Require Import Sort.
diff --git a/vfa-current/Selection.v b/vfa-current/Selection.v
index 43c91a8b2..16c0327cd 100644
--- a/vfa-current/Selection.v
+++ b/vfa-current/Selection.v
@@ -27,7 +27,7 @@
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From VFA Require Import Perm.
 Hint Constructors Permutation : core.
-From Coq Require Export Lists.List.  (* for exercises involving [List.length] *)
+From Coq Require Export List.  (* for exercises involving [List.length] *)
 
 (* ################################################################# *)
 (** * The Selection-Sort Program  *)