Remove various useless {struct} annotations

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

7 files changed, 9 insertions, 9 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 7cfad89e4..4ddae9372 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -16,7 +16,7 @@ Implicit Types m n x y : nat.
 
 (** * Propositional equality  *)
 
-Fixpoint eq_nat n m {struct n} : Prop :=
+Fixpoint eq_nat n m : Prop :=
   match n, m with
     | O, O => True
     | O, S _ => False
@@ -68,7 +68,7 @@ Defined.
 
 (** * Boolean equality on [nat] *)
 
-Fixpoint beq_nat n m {struct n} : bool :=
+Fixpoint beq_nat n m : bool :=
   match n, m with
     | O, O => true
     | O, S _ => false
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index c7e81505c..62250fc33 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -16,7 +16,7 @@ Implicit Types m n p : nat.
 
 (** * Maximum of two natural numbers *)
 
-Fixpoint max n m {struct n} : nat :=
+Fixpoint max n m : nat :=
   match n, m with
     | O, _ => m
     | S n', O => n
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 1cf6d0ed1..62948093f 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -16,7 +16,7 @@ Implicit Types m n p : nat.
 
 (** * minimum of two natural numbers *)
 
-Fixpoint min n m {struct n} : nat :=
+Fixpoint min n m : nat :=
   match n, m with
     | O, _ => 0
     | S n', O => 0
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index b6ea04c01..cd6c0a29e 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -10,7 +10,7 @@
 
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
-Fixpoint minus (n m:nat) {struct n} : nat :=
+Fixpoint minus (n m:nat) : nat :=
   match n, m with
   | O, _ => n
   | S k, O => S k
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 7b48ffe05..8346cae38 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -223,7 +223,7 @@ Qed.
     tail-recursive, whereas [mult] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
+Fixpoint mult_acc (s:nat) m n : nat :=
   match n with
     | O => s
     | S p => mult_acc (tail_plus m s) m p
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index cba87f9e5..9b7c62615 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -10,7 +10,7 @@
 
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
-Fixpoint plus (n m:nat) {struct n} : nat :=
+Fixpoint plus (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
@@ -198,7 +198,7 @@ Qed.
     tail-recursive, whereas [plus] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint tail_plus n m {struct n} : nat :=
+Fixpoint tail_plus n m : nat :=
   match n with
     | O => m
     | S n => tail_plus n (S m)
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index d142cb77f..5bc5d2a58 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -262,7 +262,7 @@ Unset Implicit Arguments.
 
 (** [n]th iteration of the function [f] *)
 
-Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A :=
   match n with
     | O => x
     | S n' => f (iter_nat n' A f x)