compatibility with POWERPC

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

7 files changed, 8 insertions, 8 deletions

diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 987d42eea..9f7de8503 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -15,7 +15,7 @@ Open Local Scope nat_scope.
 
 (** Factorial *)
 
-Fixpoint fact (n:nat) : nat :=
+Boxed Fixpoint fact (n:nat) : nat :=
   match n with
   | O => 1
   | S n => S n * fact n
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 1fdf145e9..cb9086317 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
 (**********************************************************)
 
 (**********)
-Fixpoint INR (n:nat) : R :=
+Boxed Fixpoint INR (n:nat) : R :=
   match n with
   | O => 0
   | S O => 1
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 324ebb98f..295c59ca1 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -63,7 +63,7 @@ Qed.
 (*          Power              *)
 (*******************************)
 (*********)
-Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
   match n with
   | O => 1
   | S n => r * pow r n
@@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).
 (** Sum of n first naturals    *)
 (*******************************)
 (*********)
-Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat :=
+Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat :=
   match n with
   | O => f 0%nat
   | S n' => (sum_nat_f_O f n' + f (S n'))%nat
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 4dcdebdd1..9370530a0 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -147,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
   | 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' =>
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 85f5af5e0..b29fb6a98 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -17,7 +17,7 @@ Require Import Binomial.
 Open Local Scope R_scope.
 
 (* TT Ak; 1<=k<=N *)
-Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
+Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
   match N with
   | O => 1
   | S p => prod_f_SO An p * An (S p)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 9bab638af..6d3457229 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -28,7 +28,7 @@ Section sequence.
 Variable Un : nat -> R.
 
 (*********)
-Fixpoint Rmax_N (N:nat) : R :=
+Boxed Fixpoint Rmax_N (N:nat) : R :=
   match N with
   | O => Un 0
   | S n => Rmax (Un (S n)) (Rmax_N n)
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 1be5cacc6..df750b9c6 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -15,7 +15,7 @@ Require Import SeqSeries.
 Require Import Ranalysis1.
 Open Local Scope R_scope.
 
-Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
+Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
   match N with
   | O => x
   | S n =>