diff --git a/Makefile.coq.local b/Makefile.coq.local
index 4d618052e7d1263a5c2301e0e812d6b50c0bc25e..3f5d3d8289d473d33f8adb52ed70bb7d560a3bab 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 $$(find theories/ -name "*.v" | fgrep -v theories/options.v); do \
+	$(HIDE)for FILE in $(filter-out theories/options.v,$(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