diff options
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/ConstructiveCauchyRealsPerformance.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |