docs: Add a comment in ci/test_wholefile.v

* see also #485
ProofGeneral · May 4, 2020 · 63dc6a6 · 63dc6a6
1 parent 4f25bf7
commit 63dc6a6
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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.