diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-18 19:31:40 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-18 19:31:40 +0000 |
| commit | aef3d0dceedcc277b7b5128018b0beffd31601a8 (patch) | |
| tree | 5cc44787d6ccd77889b9f3a721df7037e6a712a8 /theories/Reals/Rtrigo.v | |
| parent | 0415fea4d3c88e73d77fa49f4f032674a5687f74 (diff) | |
Removed Rtrigo's dependency on Classical.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index c637b7ab9..4981d6fdf 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. (*****************************************************************) |