COMMITED BYTECODE COMPILER

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 4dcdebdd1..d35672404 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -142,12 +142,12 @@ Record StepFun (a b:R) : Type := mkStepFun
 
 Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f).
 
-Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
+Boxed Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
   match projT2 (pre f) with
   | existT a b => a
   end.
 
-Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
+Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
   match l with
   | nil => 0
   | cons a l' =>
@@ -159,7 +159,7 @@ Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
   end.
 
 (* Integral of step functions *)
-Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R :=
+Boxed Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R :=
   match Rle_dec a b with
   | left _ => Int_SF (subdivision_val f) (subdivision f)
   | right _ => - Int_SF (subdivision_val f) (subdivision f)