From 63dc6a6bc23f2eff3e3c3bbee9e79d4097d8f139 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 21:54:31 +0200
Subject: docs: Add a comment in ci/test_wholefile.v

* see also https://github.com/ProofGeneral/PG/issues/485
---
 ci/test_wholefile.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index f947d1c5..9deee01d 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.
-- 
cgit v1.2.3