diff options
Diffstat (limited to 'theories/Reals/Rprod.v')
| -rw-r--r-- | theories/Reals/Rprod.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 6577146f..ec738996 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rprod.v,v 1.10.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rprod.v 6338 2004-11-22 09:10:51Z gregoire $ i*) Require Import Compare. Require Import Rbase. @@ -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) @@ -188,4 +188,4 @@ rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0. apply prod_neq_R0; apply INR_fact_neq_0. apply INR_eq; rewrite minus_INR; [ rewrite mult_INR; do 2 rewrite S_INR; ring | apply le_n_2n ]. -Qed.
\ No newline at end of file +Qed. |