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.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index cbf6da197..e858d2148 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -105,7 +105,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
(**********************************************************)
(**********)
-Boxed Fixpoint INR (n:nat) : R :=
+Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1