Remove various useless {struct} annotations

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

36 files changed, 102 insertions, 110 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)
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 19b6a8164..7ecfa43f2 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -233,22 +233,19 @@ Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
 Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
   Bhigh (S n) (Vshiftrepeat bool n bv).
 
-Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
-  Bvector (S n) :=
+Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftL n (BshiftL_iter n bv p') false
   end.
 
-Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
-  Bvector (S n) :=
+Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftRl n (BshiftRl_iter n bv p') false
   end.
 
-Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
-  Bvector (S n) :=
+Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftRa n (BshiftRa_iter n bv p')
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index bafbac3f1..0a35ef45e 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -130,7 +130,7 @@ Require Import List.
 
 Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
   { equiv_dec :=
-    fix aux (x : list A) y { struct x } :=
+    fix aux (x y : list A) :=
     match x, y with
       | nil, nil => in_left
       | cons hd tl, cons hd' tl' =>
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 9ad2f65cf..56fc35d89 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -357,7 +357,7 @@ Qed.
 
 (** * [equal] *)
 
-Function equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool :=
+Function equal (cmp:elt->elt->bool)(m m' : t elt) {struct m} : bool :=
   match m, m' with
    | nil, nil => true
    | (x,e)::l, (x',e')::l' =>
@@ -518,13 +518,13 @@ Variable elt':Type.
 
 (** * [map] and [mapi] *)
 
-Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' :=
+Fixpoint map (f:elt -> elt') (m:t elt) : t elt' :=
   match m with
    | nil => nil
    | (k,e)::m' => (k,f e) :: map f m'
   end.
 
-Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' :=
+Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
   match m with
    | nil => nil
    | (k,e)::m' => (k,f k e) :: mapi f m'
@@ -1171,7 +1171,7 @@ Definition t := MapS.t D.t.
 
 Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end.
 
-Fixpoint eq_list (m m' : list (X.t * D.t)) { struct m } : Prop :=
+Fixpoint eq_list (m m' : list (X.t * D.t)) : Prop :=
   match m, m' with
    | nil, nil => True
    | (x,e)::l, (x',e')::l' =>
@@ -1184,7 +1184,7 @@ Fixpoint eq_list (m m' : list (X.t * D.t)) { struct m } : Prop :=
 
 Definition eq m m' := eq_list m.(this) m'.(this).
 
-Fixpoint lt_list (m m' : list (X.t * D.t)) {struct m} : Prop :=
+Fixpoint lt_list (m m' : list (X.t * D.t)) : Prop :=
   match m, m' with
    | nil, nil => False
    | nil, _  => True
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index f5ee8b23f..56ad2ed11 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -38,7 +38,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Definition eq_sym := @sym_eq t.
   Definition eq_trans := @trans_eq t.
 
-  Fixpoint bits_lt (p q:positive) { struct p } : Prop :=
+  Fixpoint bits_lt (p q:positive) : Prop :=
    match p, q with
    | xH, xI _ => True
    | xH, _ => False
@@ -117,7 +117,7 @@ End PositiveOrderedTypeBits.
 
 (** Other positive stuff *)
 
-Fixpoint append (i j : positive) {struct i} : positive :=
+Fixpoint append (i j : positive) : positive :=
     match i with
       | xH => j
       | xI ii => xI (append ii j)
@@ -177,14 +177,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition empty : t A := Leaf.
 
-  Fixpoint is_empty (m : t A) {struct m} : bool :=
+  Fixpoint is_empty (m : t A) : bool :=
    match m with
     | Leaf => true
     | Node l None r => (is_empty l) && (is_empty r)
     | _ => false
    end.
 
-  Fixpoint find (i : positive) (m : t A) {struct i} : option A :=
+  Fixpoint find (i : positive) (m : t A) : option A :=
     match m with
     | Leaf => None
     | Node l o r =>
@@ -195,7 +195,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint mem (i : positive) (m : t A) {struct i} : bool :=
+  Fixpoint mem (i : positive) (m : t A) : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -206,7 +206,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint add (i : positive) (v : A) (m : t A) {struct i} : t A :=
+  Fixpoint add (i : positive) (v : A) (m : t A) : t A :=
     match m with
     | Leaf =>
         match i with
@@ -222,7 +222,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint remove (i : positive) (m : t A) {struct i} : t A :=
+  Fixpoint remove (i : positive) (m : t A) : t A :=
     match i with
     | xH =>
         match m with
@@ -254,8 +254,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   (** [elements] *)
 
-    Fixpoint xelements (m : t A) (i : positive) {struct m}
-             : list (positive * A) :=
+    Fixpoint xelements (m : t A) (i : positive) : list (positive * A) :=
       match m with
       | Leaf => nil
       | Node l None r =>
@@ -381,7 +380,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     exact (xelements_correct m i xH H).
   Qed.
 
-  Fixpoint xfind (i j : positive) (m : t A) {struct j} : option A :=
+  Fixpoint xfind (i j : positive) (m : t A) : option A :=
       match i, j with
       | _, xH => find i m
       | xO ii, xO jj => xfind ii jj m
@@ -394,7 +393,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v.
     Proof.
       induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
-      destruct i; congruence.
+      destruct i; simpl in *; auto.
     Qed.
 
     Lemma xelements_ii :
@@ -821,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
     Variable f : positive -> A -> B.
 
-    Fixpoint xmapi (m : t A) (i : positive) {struct m} : t B :=
+    Fixpoint xmapi (m : t A) (i : positive) : t B :=
        match m with
         | Leaf => @Leaf B
         | Node l o r => Node (xmapi l (append i (xO xH)))
@@ -906,7 +905,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Implicit Arguments Leaf [A].
 
-  Fixpoint xmap2_l (m : t A) {struct m} : t C :=
+  Fixpoint xmap2_l (m : t A) : t C :=
       match m with
       | Leaf => Leaf
       | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r)
@@ -918,7 +917,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       induction i; intros; destruct m; simpl; auto.
     Qed.
 
-  Fixpoint xmap2_r (m : t B) {struct m} : t C :=
+  Fixpoint xmap2_r (m : t B) : t C :=
       match m with
       | Leaf => Leaf
       | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r)
@@ -930,7 +929,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       induction i; intros; destruct m; simpl; auto.
     Qed.
 
-  Fixpoint _map2 (m1 : t A)(m2 : t B) {struct m1} : t C :=
+  Fixpoint _map2 (m1 : t A)(m2 : t B) : t C :=
     match m1 with
     | Leaf => xmap2_r m2
     | Node l1 o1 r1 =>
@@ -1028,7 +1027,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     rewrite xfoldi_1; reflexivity.
   Qed.
 
-  Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool :=
+  Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool :=
     match m1, m2 with
       | Leaf, _ => is_empty m2
       | _, Leaf => is_empty m1
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index e29bde236..38ed172b8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -455,13 +455,13 @@ Variable elt':Type.
 
 (** * [map] and [mapi] *)
 
-Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' :=
+Fixpoint map (f:elt -> elt') (m:t elt) : t elt' :=
   match m with
    | nil => nil
    | (k,e)::m' => (k,f e) :: map f m'
   end.
 
-Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' :=
+Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
   match m with
    | nil => nil
    | (k,e)::m' => (k,f k e) :: mapi f m'
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 9924d8a65..12a8f7a4b 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 f1baf71a7..3209860f3 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)).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 01b1c066a..b34bf65b3 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -445,7 +445,7 @@ Section Elts.
 
     Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
 
-    Fixpoint remove (x : A) (l : list A){struct l} : list A :=
+    Fixpoint remove (x : A) (l : list A) : list A :=
       match l with
 	| nil => nil
 	| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
@@ -470,7 +470,7 @@ Section Elts.
   (** [last l d] returns the last element of the list [l],
     or the default value [d] if [l] is empty. *)
 
-  Fixpoint last (l:list A) (d:A)  {struct l} : A :=
+  Fixpoint last (l:list A) (d:A) : A :=
   match l with
     | nil => d
     | a :: nil => a
@@ -479,7 +479,7 @@ Section Elts.
 
   (** [removelast l] remove the last element of [l] *)
 
-  Fixpoint removelast (l:list A) {struct l} : list A :=
+  Fixpoint removelast (l:list A) : list A :=
     match l with
       | nil =>  nil
       | a :: nil => nil
@@ -530,7 +530,7 @@ Section Elts.
 
   Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
 
-  Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
+  Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
       | nil => 0
       | y :: tl =>
@@ -686,7 +686,7 @@ Section ListOps.
 
   (**  An alternative tail-recursive definition for reverse *)
 
-  Fixpoint rev_append (l l': list A) {struct l} : list A :=
+  Fixpoint rev_append (l l': list A) : list A :=
     match l with
       | nil => l'
       | a::l => rev_append l (a::l')
@@ -1015,9 +1015,7 @@ Section Map.
   Lemma in_map :
     forall (l:list A) (x:A), In x l -> In (f x) (map l).
   Proof.
-    induction l as [| a l IHl]; simpl in |- *;
-      [ auto
-	| destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
+    induction l; firstorder (subst; auto).
   Qed.
 
   Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l.
@@ -1067,7 +1065,7 @@ Section Map.
   (** [flat_map] *)
 
   Definition flat_map (f:A -> list B) :=
-    fix flat_map (l:list A) {struct l} : list B :=
+    fix flat_map (l:list A) : list B :=
     match l with
       | nil => nil
       | cons x t => (f x)++(flat_map t)
@@ -1121,7 +1119,7 @@ Section Fold_Left_Recursor.
   Variables A B : Type.
   Variable f : A -> B -> A.
 
-  Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
+  Fixpoint fold_left (l:list B) (a0:A) : A :=
     match l with
       | nil => a0
       | cons b t => fold_left t (f a0 b)
@@ -1214,7 +1212,7 @@ End Fold_Right_Recursor.
   (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
       indexed by elts of [x], sorted in lexicographic order. *)
 
-  Fixpoint list_power (A B:Type)(l:list A) (l':list B) {struct l} :
+  Fixpoint list_power (A B:Type)(l:list A) (l':list B) :
     list (list (A * B)) :=
     match l with
       | nil => cons nil nil
@@ -1235,7 +1233,7 @@ End Fold_Right_Recursor.
   (** find whether a boolean function can be satisfied by an
        elements of the list. *)
 
-    Fixpoint existsb (l:list A) {struct l}: bool :=
+    Fixpoint existsb (l:list A) : bool :=
       match l with
 	| nil => false
 	| a::l => f a || existsb l
@@ -1275,7 +1273,7 @@ End Fold_Right_Recursor.
   (** find whether a boolean function is satisfied by
     all the elements of a list. *)
 
-    Fixpoint forallb (l:list A) {struct l} : bool :=
+    Fixpoint forallb (l:list A) : bool :=
       match l with
 	| nil => true
 	| a::l => f a && forallb l
@@ -1326,7 +1324,7 @@ End Fold_Right_Recursor.
 
   (** [partition] *)
 
-    Fixpoint partition (l:list A) {struct l} : list A * list A :=
+    Fixpoint partition (l:list A) : list A * list A :=
       match l with
 	| nil => (nil, nil)
 	| x :: tl => let (g,d) := partition tl in
@@ -1347,7 +1345,7 @@ End Fold_Right_Recursor.
 
   (** [split] derives two lists from a list of pairs *)
 
-    Fixpoint split  (l:list (A*B)) { struct l }: list A * list B :=
+    Fixpoint split (l:list (A*B)) : list A * list B :=
       match l with
 	| nil => (nil, nil)
 	| (x,y) :: tl => let (g,d) := split tl in (x::g, y::d)
@@ -1402,7 +1400,7 @@ End Fold_Right_Recursor.
       Lists given to [combine] are meant to be of same length.
       If not, [combine] stops on the shorter list *)
 
-    Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) :=
+    Fixpoint combine (l : list A) (l' : list B) : list (A*B) :=
       match l,l' with
 	| x::tl, y::tl' => (x,y)::(combine tl tl')
 	| _, _ => nil
@@ -1470,7 +1468,7 @@ End Fold_Right_Recursor.
      [combine], it adds every possible pairs, not only those at the
      same position. *)
 
-    Fixpoint list_prod (l:list A) (l':list B) {struct l} :
+    Fixpoint list_prod (l:list A) (l':list B) :
       list (A * B) :=
       match l with
 	| nil => nil
@@ -1661,7 +1659,7 @@ Section Cutting.
 
   Variable A : Type.
 
-  Fixpoint firstn (n:nat)(l:list A) {struct n} : list A :=
+  Fixpoint firstn (n:nat)(l:list A) : list A :=
     match n with
       | 0 => nil
       | S n => match l with
@@ -1670,7 +1668,7 @@ Section Cutting.
 	       end
     end.
 
-  Fixpoint skipn (n:nat)(l:list A) { struct n } : list A :=
+  Fixpoint skipn (n:nat)(l:list A) : list A :=
     match n with
       | 0 => l
       | S n => match l with
@@ -1804,7 +1802,7 @@ Section NatSeq.
   (** [seq] computes the sequence of [len] contiguous integers
       that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *)
 
-  Fixpoint seq (start len:nat) {struct len} : list nat :=
+  Fixpoint seq (start len:nat) : list nat :=
     match len with
       | 0 => nil
       | S len => start :: seq (S start) len
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index d8a8183f3..e6c3a435b 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -27,7 +27,7 @@ Section first_definitions.
 
   Definition empty_set : set := nil.
 
-  Fixpoint set_add (a:A) (x:set) {struct x} : set :=
+  Fixpoint set_add (a:A) (x:set) : set :=
     match x with
     | nil => a :: nil
     | a1 :: x1 =>
@@ -38,7 +38,7 @@ Section first_definitions.
     end.
 
 
-  Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=
+  Fixpoint set_mem (a:A) (x:set) : bool :=
     match x with
     | nil => false
     | a1 :: x1 =>
@@ -49,7 +49,7 @@ Section first_definitions.
     end.
 
   (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
-  Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
+  Fixpoint set_remove (a:A) (x:set) : set :=
     match x with
     | nil => empty_set
     | a1 :: x1 =>
@@ -67,14 +67,14 @@ Section first_definitions.
           if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
     end.
 
-  Fixpoint set_union (x y:set) {struct y} : set :=
+  Fixpoint set_union (x y:set) : set :=
     match y with
     | nil => x
     | a1 :: y1 => set_add a1 (set_union x y1)
     end.
 
   (** returns the set of all els of [x] that does not belong to [y] *)
-  Fixpoint set_diff (x y:set) {struct x} : set :=
+  Fixpoint set_diff (x y:set) : set :=
     match x with
     | nil => nil
     | a1 :: x1 =>
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index e10ad325f..d906cfa44 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -80,7 +80,7 @@ Variable f: forall n, A n.
 Inductive memo_val: Type :=
   memo_mval: forall n, A n -> memo_val.
 
-Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
+Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
   match n, m return {n = m} + {True} with
   | 0, 0 =>left True (refl_equal 0)
   | 0, S m1 => right (0 = S m1) I
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index ace157749..3fa053b7f 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -29,7 +29,7 @@ Definition tl (x:Stream) := match x with
                             end.
 
 
-Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
+Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
   match n with
   | O => s
   | S m => Str_nth_tl m (tl s)
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 5185f2c53..da3018a48 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -97,7 +97,7 @@ Qed.
 (****************************************)
 
 (* length is defined in List *)
-Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
+Fixpoint Length_l (l:list A) (n:nat) : nat :=
   match l with
   | nil => n
   | _ :: m => Length_l m (S n)
@@ -146,7 +146,7 @@ Hint Resolve allS_nil allS_cons.
 
 Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
 
-Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
+Fixpoint mem (a:A) (l:list A) : bool :=
   match l with
   | nil => false
   | b :: m => if eqA_dec a b then true else mem a m
@@ -201,7 +201,7 @@ Lemma nth_le_length :
 induction 1; simpl in |- *; auto with arith.
 Qed.
 
-Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A :=
+Fixpoint Nth_func (l:list A) (n:nat) : Exc A :=
   match l, n with
   | a :: _, S O => value a
   | _ :: l', S (S p) => Nth_func l' (S p)
@@ -237,7 +237,7 @@ Qed.
 Require Import Minus.
 Require Import DecBool.
 
-Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat :=
+Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat :=
   match l with
   | nil => fun p => error
   | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p))
@@ -359,7 +359,7 @@ End Find_sec.
 Section Assoc_sec.
 
 Variable B : Type.
-Fixpoint assoc (a:A) (l:list (A * B)) {struct l} :
+Fixpoint assoc (a:A) (l:list (A * B)) :
  Exc B :=
   match l with
   | nil => error
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index a35682767..2456e1706 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -17,7 +17,7 @@ Require Import BinNat.
 
 (** [xor] *)
 
-Fixpoint Pxor (p1 p2:positive) {struct p1} : N :=
+Fixpoint Pxor (p1 p2:positive) : N :=
   match p1, p2 with
   | xH, xH => N0
   | xH, xO p2 => Npos (xI p2)
@@ -409,7 +409,7 @@ Qed.
 
 (** a lexicographic order on bits, starting from the lowest bit *)
 
-Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool :=
+Fixpoint Nless_aux (a a':N) (p:positive) : bool :=
   match p with
   | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p'
   | _ => andb (negb (Nbit0 a)) (Nbit0 a')
@@ -579,7 +579,7 @@ Definition N2Bv (n:N) : Bvector (Nsize n) :=
     | Npos p => P2Bv p
   end.
 
-Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N :=
+Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vnil => N0
     | Vcons false n bv => Ndouble (Bv2N n bv)
@@ -629,7 +629,7 @@ Qed.
 (** To state nonetheless a second result about composition of
  conversions, we define a conversion on a given number of bits : *)
 
-Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n :=
+Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
  match n return Bvector n with
    | 0 => Bnil
    | S n => match a with
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 9b7ea0474..c4d06fd72 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -27,7 +27,7 @@ Section Well_founded.
 
   Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
 
-  Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
+  Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x :=
     F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y)
       (Acc_inv r (proj2_sig y))).
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 266d81e01..34d6267e3 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -449,7 +449,7 @@ Qed.
 
 (** Rational to the n-th power *)
 
-Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc :=
+Fixpoint Qcpower (q:Qc)(n:nat) : Qc :=
   match n with
     | O => 1
     | S n => q * (Qcpower q n)
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index a95985d3b..545bd68b2 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 11be9772e..7371c8acf 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 63684c1f3..ae2c3d77f 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 e7f0375f0..f9b1b890f 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 c9fb56292..c7d1893be 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 f02b77564..bb3df6bb8 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)
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 87d8e1350..1f90c06cf 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -59,7 +59,7 @@ Defined.
    looking at the last n bits, ie z mod 2^n *)
 
 Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive)
-  (n : nat) {struct n} : ascii :=
+  (n : nat) : ascii :=
   match n with
     | O => res
     | S n1 =>
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 21c0a15e9..15f298218 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -38,7 +38,7 @@ Defined.
 
 Reserved Notation "x ++ y" (right associativity, at level 60).
 
-Fixpoint append (s1 s2 : string) {struct s1} : string :=
+Fixpoint append (s1 s2 : string) : string :=
   match s1 with
   | EmptyString => s2
   | String c s1' => String c (s1' ++ s2)
@@ -122,7 +122,7 @@ Qed.
     at position [n] and of length [m];
     if this does not make sense it returns [""] *)
 
-Fixpoint substring (n m : nat) (s : string) {struct s} : string :=
+Fixpoint substring (n m : nat) (s : string) : string :=
   match n, m, s with
   | 0, 0, _ => EmptyString
   | 0, S m', EmptyString => s
@@ -205,7 +205,7 @@ Qed.
 (** Test if, starting at position [n], [s1] occurs in [s2]; if
     so it returns the position *)
 
-Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
+Fixpoint index (n : nat) (s1 s2 : string) : option nat :=
   match s2, n with
   | EmptyString, 0 =>
       match s1 with
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
index c73b6f091..88d573bb0 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 0929d965a..08cc564de 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 bc35ba405..f3e656970 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 93ac74d54..178ae5f15 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 23a2e510f..2a2751c9d 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 39aab6331..1d9b3dfc9 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' =>