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 24eba0cef..10dd8eb83 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -14,7 +14,7 @@ Require Rfunctions. Require Rseries. Require PartSum. Require Binomial. -V7only [Import R_scope.]. +V7only [Import R_scope.]. Open Scope R_scope. (* TT Ak; 1<=k<=N *) Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of |