diff options
Diffstat (limited to 'theories/Reals/Rprod.v')
| -rw-r--r-- | theories/Reals/Rprod.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 76d66ca06..12258d6b5 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -15,7 +15,7 @@ Require Import Binomial. Open Local Scope R_scope. (** TT Ak; 0<=k<=N *) -Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := +Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := match N with | O => f O | S p => prod_f_R0 f p * f (S p) |