From 3bc39fbd726676e5d1a650b683f0b5d72dbd1c3b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:23:58 +0200
Subject: fix: Tweak comments and workaround ProofGeneral/PG#485

---
 ci/test_wholefile.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'ci')

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index 0a87d9a6..d8b57d20 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -1,4 +1,4 @@
-(*taking from coq.inria.fr *)
+(* taken from https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html *)
 
 Require Export ArithRing.
 Require Export Compare_dec.
@@ -133,6 +133,7 @@ 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.
@@ -141,5 +142,3 @@ apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 * p);
  rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with *.
 apply new_equality; auto.
 Qed.
-
-(*end here*)
-- 
cgit v1.2.3