From fac5fb7a4ebfa46816faa2f3ebdfef4443b9fa75 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Sep 2020 11:16:45 +0200
Subject: [PATCH] improve options-import check

---
 Makefile.coq.local | 2 +-
 theories/options.v | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 3f5d3d828..2f940e8cc 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 a228ffdf6..895e51f00 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.
+*)
-- 
GitLab