diff options
author | 2004-11-12 16:40:39 +0000 | |
---|---|---|
committer | 2004-11-12 16:40:39 +0000 | |
commit | f987a343850df4602b3d8020395834d22eb1aea3 (patch) | |
tree | c9c23771714f39690e9dc42ce0c58653291d3202 /theories/Reals/Rfunctions.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/Rfunctions.v')
-rw-r--r-- | theories/Reals/Rfunctions.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 3e1a9262d..324ebb98f 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -63,7 +63,7 @@ Qed. (* Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := +Fixpoint pow (r:R) (n:nat) {struct n} : R := match n with | O => 1 | S n => r * pow r n @@ -527,7 +527,7 @@ Qed. Ltac case_eq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. -Boxed Definition powerRZ (x:R) (n:Z) := +Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 | Zpos p => x ^ nat_of_P p @@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** Sum of n first naturals *) (*******************************) (*********) -Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat @@ -690,7 +690,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x). (** Sum *) (*******************************) (*********) -Boxed Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := match N with | O => f 0%nat | S i => sum_f_R0 f i + f (S i) |