From 18544983e1b2a342c8bbcbd3c51003b11453213f Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Thu, 30 Apr 2020 18:27:21 +0200
Subject: Replace QSeqEquiv by QCauchySeq, simplify proofs.

Force Cauchy modulus equal to identity, make division transparent

Fix test
---
 test-suite/complexity/ConstructiveCauchyRealsPerformance.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
index c901334da9..f3bc1767da 100644
--- a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
+++ b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
@@ -105,7 +105,7 @@ Proof.
 Qed.
 
 Lemma approx_sqrt_Q_cauchy :
-  forall q:Q, QCauchySeq (approx_sqrt_Q q) id.
+  forall q:Q, QCauchySeq (approx_sqrt_Q q).
 Proof.
   intro q. destruct q as [k j]. destruct k.
   - intros n a b H H0. reflexivity.
-- 
cgit v1.2.3