diff --git a/theories/base.v b/theories/base.v
index 2c42f50fa62fb254a25588bed5522e4a6f8e3ef2..603fe11a829333a84def3835562361a7a752ebe0 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,9 +10,9 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
-From stdpp Require Import options.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+From stdpp Require Import options.
 
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
diff --git a/theories/prelude.v b/theories/prelude.v
index aff80807e9a8c62761ab2a2fbcf0d25cb5c766f3..9c18d5eef37d92341f80527275841733a676c2b2 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -12,8 +12,4 @@ From stdpp Require Export
   list
   list_numbers
   lexico.
-
-(* "Fake" import to whitelist this file for the check that ensures we import
-this file everywhere.
 From stdpp Require Import options.
-*)