diff options
Diffstat (limited to 'theories/Reals/Rprod.v')
| -rw-r--r-- | theories/Reals/Rprod.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 160d9be4c..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) @@ -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. |