From 6f2f532af7d065779bca1e7c994d065f50338d9c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:54:43 +0200
Subject: test: Remove "Proof." workaround

---
 ci/test_wholefile.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index d8b57d20..f947d1c5 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -133,7 +133,6 @@ Hint Resolve lt_le_weak comparison2: sqrt.
 
 Theorem sqrt2_not_rational :
  forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
-Proof.
 intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
 clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq));
  intros Hlt_O_q Heq.
-- 
cgit v1.2.3