diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index c8d4924bf24416a8ce6d41b24c5766f63d19cb8e..67eef817ff135946e050e0ed2e2544af05b7ace0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -46,6 +46,8 @@ Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
 Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
 *all* the `.ref` files.
 
+If you want to compile without tests run `make NO_TEST=1`.
+
 ## How to measure the timing effect on a reverse dependency
 
 So say you did a change in Iris, and want to know how it affects [lambda-rust]
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 9ceafe4c78e77fadbe75be6184269b6b1619b6eb..d9758f0333e990d69edfd6c648744556c0aec62e 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -1,3 +1,9 @@
+# use NO_TEST=1 to skip the tests
+NO_TEST:=
+
+# use MAKE_REF=1 to generate new reference files
+MAKE_REF:=
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: $(if $(NO_TEST),,test)