Remove various useless {struct} annotations

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

2 files changed, 5 insertions, 6 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 9924d8a658..12a8f7a4b0 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -89,7 +89,7 @@ Hint Resolve n_Sn: core.
 
 (** Addition *)
 
-Fixpoint plus (n m:nat) {struct n} : nat :=
+Fixpoint plus (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
@@ -129,7 +129,7 @@ Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
 
 (** Multiplication *)
 
-Fixpoint mult (n m:nat) {struct n} : nat :=
+Fixpoint mult (n m:nat) : nat :=
   match n with
   | O => 0
   | S p => m + p * m
@@ -160,7 +160,7 @@ Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
 
 (** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
-Fixpoint minus (n m:nat) {struct n} : nat :=
+Fixpoint minus (n m:nat) : nat :=
   match n, m with
   | O, _ => n
   | S k, O => n
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index f1baf71a7f..3209860f34 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -72,7 +72,7 @@ Section Well_founded.
   Variable P : A -> Type.
   Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-  Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+  Fixpoint Fix_F (x:A) (a:Acc x) : P x :=
     F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
 
   Scheme Acc_inv_dep := Induction for Acc Sort Prop.
@@ -129,8 +129,7 @@ Section Well_founded_2.
       forall (x:A) (x':B),
         (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
 
-  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} :
-   P x x' :=
+  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) : P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
          Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).