diff --git a/Makefile.coq.local b/Makefile.coq.local
index 3f5d3d8289d473d33f8adb52ed70bb7d560a3bab..2f940e8cca3b7f0f7c80bece8bff5ee6a764997b 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -13,7 +13,7 @@ NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
 # Make sure everything imports the options.
-	$(HIDE)for FILE in $(filter-out theories/options.v,$(VFILES)); do \
+	$(HIDE)for FILE in $(VFILES); do \
 	  if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; exit 1; fi \
 	done
 .PHONY: test
diff --git a/theories/options.v b/theories/options.v
index a228ffdf6c781a64937bf2104f48c5b08d89e3b6..895e51f007c38d235f66bb186ce7ea14ceef50bf 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -5,3 +5,8 @@ but not transitively. *)
 
 Export Set Default Proof Using "Type".
 Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
+
+(* "Fake" import to whitelist this file for the check that ensures we import
+this file everywhere.
+From iris Require Import options.
+*)