Changement dans les boxed values .

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 30dfa6274..d850d7f89 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 *)
-Boxed Definition Rln (y:posreal) : R :=
+Definition Rln (y:posreal) : R :=
   match ln_exists (pos y) (cond_pos y) with
   | existT a b => a
   end.
 
 (* Extension on R *)
-Boxed Definition ln (x:R) : R :=
+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                   *)
 (******************************************************************)
  
-Boxed Definition Rpower (x y:R) := exp (y * ln x).
+Definition Rpower (x y:R) := exp (y * ln x).
 
 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.