diff options
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 8f01d7d03f..259e1ac04b 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -122,8 +122,8 @@ Arguments INR n%nat. Definition IZR (z:Z) : R := match z with | Z0 => 0 - | Zpos n => INR (nat_of_P n) - | Zneg n => - INR (nat_of_P n) + | Zpos n => INR (Pos.to_nat n) + | Zneg n => - INR (Pos.to_nat n) end. Arguments IZR z%Z. |