Remove various useless {struct} annotations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 14 insertions, 14 deletions

diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index a95985d3b1..545bd68b2c 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -16,7 +16,7 @@ Inductive Rlist : Type :=
 | nil : Rlist
 | cons : R -> Rlist -> Rlist.
 
-Fixpoint In (x:R) (l:Rlist) {struct l} : Prop :=
+Fixpoint In (x:R) (l:Rlist) : Prop :=
   match l with
     | nil => False
     | cons a l' => x = a \/ In x l'
@@ -70,7 +70,7 @@ Proof.
   reflexivity.
 Qed.
 
-Fixpoint AbsList (l:Rlist) (x:R) {struct l} : Rlist :=
+Fixpoint AbsList (l:Rlist) (x:R) : Rlist :=
   match l with
     | nil => nil
     | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x)
@@ -150,7 +150,7 @@ Proof.
   left; reflexivity.
 Qed.
 
-Fixpoint pos_Rl (l:Rlist) (i:nat) {struct l} : R :=
+Fixpoint pos_Rl (l:Rlist) (i:nat) : R :=
   match l with
     | nil => 0
     | cons a l' => match i with
@@ -221,7 +221,7 @@ Qed.
 Definition ordered_Rlist (l:Rlist) : Prop :=
   forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i).
 
-Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist :=
+Fixpoint insert (l:Rlist) (x:R) : Rlist :=
   match l with
     | nil => cons x nil
     | cons a l' =>
@@ -231,25 +231,25 @@ Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist :=
       end
   end.
 
-Fixpoint cons_Rlist (l k:Rlist) {struct l} : Rlist :=
+Fixpoint cons_Rlist (l k:Rlist) : Rlist :=
   match l with
     | nil => k
     | cons a l' => cons a (cons_Rlist l' k)
   end.
 
-Fixpoint cons_ORlist (k l:Rlist) {struct k} : Rlist :=
+Fixpoint cons_ORlist (k l:Rlist) : Rlist :=
   match k with
     | nil => l
     | cons a k' => cons_ORlist k' (insert l a)
   end.
 
-Fixpoint app_Rlist (l:Rlist) (f:R -> R) {struct l} : Rlist :=
+Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist :=
   match l with
     | nil => nil
     | cons a l' => cons (f a) (app_Rlist l' f)
   end.
 
-Fixpoint mid_Rlist (l:Rlist) (x:R) {struct l} : Rlist :=
+Fixpoint mid_Rlist (l:Rlist) (x:R) : Rlist :=
   match l with
     | nil => nil
     | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 11be9772e3..7371c8acf3 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -676,7 +676,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 :=
+Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
   match n with
     | O => f 0%nat
     | S n' => (sum_nat_f_O f n' + f (S n'))%nat
@@ -696,7 +696,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).
 (** *          Sum             *)
 (*******************************)
 (*********)
-Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
+Fixpoint sum_f_R0 (f:nat -> R) (N:nat) : R :=
   match N with
     | O => f 0%nat
     | S i => sum_f_R0 f i + f (S i)
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 63684c1f34..ae2c3d77f8 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -466,7 +466,7 @@ Proof.
                       elim (Rlt_irrefl _ H7) ] ].
 Qed.
 
-Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist :=
+Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist :=
   match N with
     | O => cons y nil
     | S p => cons x (SubEquiN p (x + del) y del)
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index e7f0375f03..f9b1b890f7 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -149,7 +149,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
     | existT a b => a
   end.
 
-Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
+Boxed Fixpoint Int_SF (l k:Rlist) : R :=
   match l with
     | nil => 0
     | cons a l' =>
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index c9fb56292a..c7d1893be0 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -10,7 +10,7 @@
 
 Require Import Rdefinitions.
 
-Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+Fixpoint pow (r:R) (n:nat) : R :=
   match n with
     | O => R1
     | S n => Rmult r (pow r n)
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index f02b77564f..bb3df6bb8e 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -17,7 +17,7 @@ Require Import Binomial.
 Open Local Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
-Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
+Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
   match N with
     | O => f O
     | S p => prod_f_R0 f p * f (S p)