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, 8 insertions, 9 deletions

diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
index c73b6f0916..88d573bb00 100644
--- a/theories/ZArith/ZOdiv_def.v
+++ b/theories/ZArith/ZOdiv_def.v
@@ -17,7 +17,7 @@ Definition NPgeb (a:N)(b:positive) :=
    | Npos na => match Pcompare na b Eq with Lt => false | _ => true end
   end.
 
-Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N :=
+Fixpoint Pdiv_eucl (a b:positive) : N * N :=
   match a with
     | xH =>
        match b with xH => (1, 0)%N | _ => (0, 1)%N end
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 0929d965ac..08cc564de5 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -160,7 +160,7 @@ Qed.
 
 Require Import List.
 
-Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z :=
+Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z :=
   match l with
     | nil => acc
     | _ :: l => Zlength_aux (Zsucc acc) A l
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index bc35ba4052..f3e656970e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -35,8 +35,7 @@ Open Local Scope Z_scope.
 
 *)
 
-Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} :
-  Z * Z :=
+Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z :=
   match a with
     | xH => if Zge_bool b 2 then (0, 1) else (1, 0)
     | xO a' =>
@@ -1071,7 +1070,7 @@ Qed.
 
 (** * A direct way to compute Zmod *)
 
-Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z  :=
+Fixpoint Zmod_POS (a : positive) (b : Z) : Z  :=
   match a with
    | xI a' =>
       let r := Zmod_POS a' b in
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 93ac74d544..178ae5f158 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -20,7 +20,7 @@ Open Local Scope Z_scope.
 
 (** [n]th iteration of the function [f] *)
 
-Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A :=
   match n with
     | xH => f x
     | xO n' => iter_pos n' A f (iter_pos n' A f x)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 23a2e510f4..2a2751c9db 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -892,7 +892,7 @@ Qed.
 
 Open Scope positive_scope.
 
-Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive :=
+Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
   match n with
     | O => 1
     | S n =>
@@ -1255,7 +1255,7 @@ Qed.
 
 Open Scope positive_scope.
 
-Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) :=
+Fixpoint Pggcdn (n: nat) (a b : positive) : (positive*(positive*positive)) :=
   match n with
     | O => (1,(a,b))
     | S n =>
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 39aab63317..1d9b3dfc97 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -294,7 +294,7 @@ Qed.
 
 (** A direct way to compute Zpower modulo **)
 
-Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z :=
+Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z :=
   match m with
    | xH => a mod n
    | xO m' =>