diff options
Diffstat (limited to 'theories/Reals/Rpow_def.v')
| -rw-r--r-- | theories/Reals/Rpow_def.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index 791718a45..f331bb203 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -10,6 +10,6 @@ Require Import Rdefinitions. Fixpoint pow (r:R) (n:nat) : R := match n with - | O => R1 + | O => 1 | S n => Rmult r (pow r n) end. |