COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 7ef2ed69a..30dfa6274 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -195,13 +195,13 @@ apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H;
 Qed.
 
 (* Definition of log R+* -> R *)
-Definition Rln (y:posreal) : R :=
+Boxed Definition Rln (y:posreal) : R :=
   match ln_exists (pos y) (cond_pos y) with
   | existT a b => a
   end.
 
 (* Extension on R *)
-Definition ln (x:R) : R :=
+Boxed Definition ln (x:R) : R :=
   match Rlt_dec 0 x with
   | left a => Rln (mkposreal x a)
   | right a => 0
@@ -377,7 +377,7 @@ Qed.
 (*                        Definition of  Rpower                   *)
 (******************************************************************)
  
-Definition Rpower (x y:R) := exp (y * ln x).
+Boxed Definition Rpower (x y:R) := exp (y * ln x).
 
 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 
@@ -658,4 +658,4 @@ apply derivable_pt_lim_const with (a := y).
 apply derivable_pt_lim_id.
 ring.
 apply derivable_pt_lim_exp.
-Qed.
\ No newline at end of file
+Qed.