diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-12 16:40:39 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-12 16:40:39 +0000 |
| commit | f987a343850df4602b3d8020395834d22eb1aea3 (patch) | |
| tree | c9c23771714f39690e9dc42ce0c58653291d3202 /theories/Reals/Raxioms.v | |
| parent | 41095b1f02abac5051ab61a91080550bebbb3a7e (diff) | |
Changement dans les boxed values .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1acd611d5..1fdf145e9 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. (**********************************************************) (**********) -Boxed Fixpoint INR (n:nat) : R := +Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 @@ -121,7 +121,7 @@ Arguments Scope INR [nat_scope]. (**********************************************************) (**********) -Boxed Definition IZR (z:Z) : R := +Definition IZR (z:Z) : R := match z with | Z0 => 0 | Zpos n => INR (nat_of_P n) |