aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Raxioms.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Raxioms.v')
-rw-r--r--theories/Reals/Raxioms.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 1fdf145e9..1acd611d5 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
(**********************************************************)
(**********)
-Fixpoint INR (n:nat) : R :=
+Boxed Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1
@@ -121,7 +121,7 @@ Arguments Scope INR [nat_scope].
(**********************************************************)
(**********)
-Definition IZR (z:Z) : R :=
+Boxed Definition IZR (z:Z) : R :=
match z with
| Z0 => 0
| Zpos n => INR (nat_of_P n)