From aef3d0dceedcc277b7b5128018b0beffd31601a8 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Thu, 18 Feb 2010 19:31:40 +0000
Subject: Removed Rtrigo's dependency on Classical.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rtrigo.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index c637b7ab94..4981d6fdf1 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -18,7 +18,6 @@ Require Export Cos_rel.
 Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
-Require Import Classical_Prop.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
@@ -372,7 +371,11 @@ Qed.
 
 Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.
 Proof.
-  intro; apply not_and_or; apply cos_sin_0.
+  intros x.
+  destruct (Req_dec (cos x) 0). 2: now left.
+  right. intros H'.
+  apply (cos_sin_0 x).
+  now split.
 Qed.
 
 (*****************************************************************)
-- 
cgit v1.2.3