Remove various useless {struct} annotations

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

3 files changed, 22 insertions, 23 deletions

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'