diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /theories/Reals/Rtrigo_def.v | |
parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 170431ecd..3d848a948 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -35,7 +35,7 @@ unfold Pser, exp_in in |- *. trivial. Defined. -Definition exp (x:R) : R := projT1 (exist_exp x). +Boxed Definition exp (x:R) : R := projT1 (exist_exp x). Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0. intros; apply pow_ne_zero. @@ -235,7 +235,7 @@ Qed. (* Definition of cosinus *) (*************************) -Definition cos (x:R) : R := +Boxed Definition cos (x:R) : R := match exist_cos (Rsqr x) with | existT a b => a end. @@ -356,7 +356,7 @@ Qed. (***********************) (* Definition of sinus *) -Definition sin (x:R) : R := +Boxed Definition sin (x:R) : R := match exist_sin (Rsqr x) with | existT a b => x * a end. @@ -409,4 +409,4 @@ apply H. exact (projT2 exist_cos0). assert (H := projT2 (exist_cos (Rsqr 0))); unfold cos in |- *; pattern 0 at 1 in |- *; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. -Qed.
\ No newline at end of file +Qed. |