diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index f947d1c5b..9deee01dd 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -1,4 +1,6 @@
 (* taken from https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html *)
+(* Note: this file contains no "Proof" command (invariant to preserve)
+   in order to exercise 070_coq-test-regression-wholefile-no-proof. *)
 
 Require Export ArithRing.
 Require Export Compare_dec.