Imported Upstream version 8.5~beta1+dfsg

9 files changed, 75 insertions, 88 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index db12ee31..e1fc454a 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -38,7 +38,6 @@ Unset Strict Implicit.
 (* for nicer extraction, we create inductive principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** * Ops : the pure functions *)
 
@@ -307,13 +306,13 @@ Include MSetGenTree.Props X I.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
 
 (* Sometimes functional induction will expose too much of
-   a tree structure. The following tactic allows to factor back
+   a tree structure. The following tactic allows factoring back
    a Node whose internal parts occurs nowhere else. *)
 
 (* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *)
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index eefd2951..f2555791 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -15,7 +15,7 @@
 (** This file implements a decision procedure for a certain
     class of propositions involving finite sets.  *)
 
-Require Import Decidable DecidableTypeEx MSetFacts.
+Require Import Decidable Setoid DecidableTypeEx MSetFacts.
 
 (** First, a version for Weak Sets in functorial presentation *)
 
@@ -115,8 +115,8 @@ the above form:
       not affect the namespace if you import the enclosing
       module [Decide]. *)
   Module MSetLogicalFacts.
-    Require Export Decidable.
-    Require Export Setoid.
+    Export Decidable.
+    Export Setoid.
 
     (** ** Lemmas and Tactics About Decidable Propositions *)
 
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 4f0d93fb..ae20edc8 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -819,8 +819,7 @@ Proof.
 intros.
 rewrite for_all_exists in H; auto.
 rewrite negb_true_iff in H.
-elim (@for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto.
-elim p;intros.
+destruct (@for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,[]); auto.
 exists x;split;auto.
 rewrite <-negb_false_iff; auto.
 Qed.
@@ -856,7 +855,7 @@ intros.
 rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite fold_add; auto with *).
+intros. do 3 (rewrite fold_add; auto with *).
 do 3 rewrite fold_empty;auto.
 Qed.
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 704ff31b..154c2384 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -27,14 +27,13 @@
      - min_elt max_elt choose
 *)
 
-Require Import Orders OrdersFacts MSetInterface NPeano.
+Require Import Orders OrdersFacts MSetInterface PeanoNat.
 Local Open Scope list_scope.
 Local Open Scope lazy_bool_scope.
 
 (* For nicer extraction, we create induction principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 Module Type InfoTyp.
  Parameter t : Set.
@@ -341,7 +340,7 @@ Module Import MX := OrderedTypeFacts X.
 Scheme tree_ind := Induction for tree Sort Prop.
 Scheme bst_ind := Induction for bst Sort Prop.
 
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree.
 Local Hint Constructors InT bst.
@@ -378,7 +377,7 @@ Ltac invtree f :=
 
 Ltac inv := inv_ok; invtree InT.
 
-Ltac intuition_in := repeat progress (intuition; inv).
+Ltac intuition_in := repeat (intuition; inv).
 
 (** Helper tactic concerning order of elements. *)
 
@@ -963,13 +962,16 @@ Proof. firstorder. Qed.
 Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
 Proof.
  unfold eq, Equal, L.eq; intros.
- setoid_rewrite elements_spec1; firstorder.
+ setoid_rewrite elements_spec1.
+ firstorder. 
 Qed.
 
 Definition lt (s1 s2 : tree) : Prop :=
  exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
    /\ L.lt (elements s1') (elements s2').
 
+Declare Equivalent Keys L.eq equivlistA.
+
 Instance lt_strorder : StrictOrder lt.
 Proof.
  split.
@@ -1017,7 +1019,7 @@ Lemma flatten_e_elements :
  forall l x r c e,
  elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
 Proof.
- intros; simpl. now rewrite elements_node, app_ass.
+ intros. now rewrite elements_node, app_ass.
 Qed.
 
 Lemma cons_1 : forall s e,
@@ -1051,7 +1053,7 @@ Lemma compare_cont_Cmp : forall s1 cont e2 l,
  (forall e, Cmp (cont e) l (flatten_e e)) ->
  Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
 Proof.
- induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; simpl; intros; auto.
+ induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; intros; auto.
  rewrite elements_node, app_ass; simpl.
  apply Hl1; auto. clear e2. intros [|x2 r2 e2].
  simpl; auto.
@@ -1063,9 +1065,9 @@ Lemma compare_Cmp : forall s1 s2,
  Cmp (compare s1 s2) (elements s1) (elements s2).
 Proof.
  intros; unfold compare.
- rewrite (app_nil_end (elements s1)).
+ rewrite <- (app_nil_r (elements s1)).
  replace (elements s2) with (flatten_e (cons s2 End)) by
-  (rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
+  (rewrite cons_1; simpl; rewrite app_nil_r; auto).
  apply compare_cont_Cmp; auto.
  intros.
  apply compare_end_Cmp; auto.
@@ -1129,14 +1131,14 @@ Proof.
 Qed.
 
 Lemma maxdepth_log_cardinal s : s <> Leaf ->
- log2 (cardinal s) < maxdepth s.
+ Nat.log2 (cardinal s) < maxdepth s.
 Proof.
  intros H.
  apply Nat.log2_lt_pow2. destruct s; simpl; intuition.
  apply maxdepth_cardinal.
 Qed.
 
-Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)).
+Lemma mindepth_log_cardinal s : mindepth s <= Nat.log2 (S (cardinal s)).
 Proof.
  apply Nat.log2_le_pow2. auto with arith.
  apply mindepth_cardinal.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 6778deff..bd881168 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -431,7 +431,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
  (** We avoid creating induction principles for the Record *)
  Local Unset Elimination Schemes.
- Local Unset Case Analysis Schemes.
 
  Definition elt := E.t.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d9b1fd9b..fb0d1ad9 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -56,7 +56,7 @@ Module Ops (X:OrderedType) <: WOps X.
 
   Definition singleton (x : elt) := x :: nil.
 
-  Fixpoint remove x s :=
+  Fixpoint remove x s : t :=
     match s with
     | nil => nil
     | y :: l =>
@@ -228,16 +228,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
 
-  (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Existing Instance X.eq_equiv.
+  Hint Extern 20 => solve [order].
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
-  Hint Resolve @ok.
+  Hint Resolve ok.
   Hint Unfold Ok.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -343,7 +341,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   induction s; simpl; intros.
   intuition. inv; auto.
   elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
-  left; order.
   Qed.
 
   Lemma remove_inf :
@@ -402,8 +399,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
   repeat rewrite <- isok_iff; revert s s'.
-  induction2; constructors; try apply @ok; auto.
-  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+  induction2; constructors; try apply @ok; auto. 
+  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.
   change (Inf x' (union (x :: l) l')); auto.
   Qed.
 
@@ -412,7 +409,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    In x (union s s') <-> In x s \/ In x s'.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
-  left; order.
   Qed.
 
   Lemma inter_inf :
@@ -440,7 +436,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
    try sort_inf_in; try order.
-  left; order.
   Qed.
 
   Lemma diff_inf :
@@ -477,7 +472,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    equal s s' = true <-> Equal s s'.
   Proof.
   induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
-  intuition.
+  intuition reflexivity. 
   split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
   split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
   inv.
@@ -825,7 +820,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
 
   Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
   Proof.
-  induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
+  induction s as [|x s IH]; intros [|x' s']; simpl; intuition. 
   elim_compare x x'; auto.
   Qed.
 
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index e500602f..25a8c162 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -19,14 +19,9 @@
 Require Import Bool BinPos Orders MSetInterface.
 
 Set Implicit Arguments.
-
 Local Open Scope lazy_bool_scope.
 Local Open Scope positive_scope.
-
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
-Local Unset Boolean Equality Schemes.
-
 
 (** Even if [positive] can be seen as an ordered type with respect to the
   usual order (see above), we can also use a lexicographic order over bits
@@ -98,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
 
-  Definition elt := positive.
+  Definition elt := positive : Type.
 
   Inductive tree :=
     | Leaf : tree
@@ -106,9 +101,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Scheme tree_ind := Induction for tree Sort Prop.
 
-  Definition t := tree.
+  Definition t := tree : Type.
 
-  Definition empty := Leaf.
+  Definition empty : t := Leaf.
 
   Fixpoint is_empty (m : t) : bool :=
    match m with
@@ -116,7 +111,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     | Node l b r => negb b &&& is_empty l &&& is_empty r
    end.
 
-  Fixpoint mem (i : positive) (m : t) : bool :=
+  Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -147,13 +142,13 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** helper function to avoid creating empty trees that are not leaves *)
 
-  Definition node l (b: bool) r :=
+  Definition node (l : t) (b: bool) (r : t) : t :=
     if b then Node l b r else
      match l,r with
        | Leaf,Leaf => Leaf
        | _,_ => Node l false r end.
 
-  Fixpoint remove (i : positive) (m : t) : t :=
+  Fixpoint remove (i : positive) (m : t) {struct m} : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -164,7 +159,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint union (m m': t) :=
+  Fixpoint union (m m': t) : t :=
     match m with
       | Leaf => m'
       | Node l o r =>
@@ -174,7 +169,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint inter (m m': t) :=
+  Fixpoint inter (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -184,7 +179,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint diff (m m': t) :=
+  Fixpoint diff (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -216,7 +211,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** reverses [y] and concatenate it with [x] *)
 
-  Fixpoint rev_append y x :=
+  Fixpoint rev_append (y x : elt) : elt :=
     match y with
       | 1 => x
       | y~1 => rev_append y x~1
@@ -267,14 +262,14 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       end.
     Definition exists_ m := xexists m 1.
 
-    Fixpoint xfilter (m : t) (i : positive) :=
+    Fixpoint xfilter (m : t) (i : positive) : t :=
       match m with
         | Leaf => Leaf
         | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
       end.
     Definition filter m := xfilter m 1.
 
-    Fixpoint xpartition (m : t) (i : positive) :=
+    Fixpoint xpartition (m : t) (i : positive) : t * t :=
       match m with
         | Leaf => (Leaf,Leaf)
         | Node l o r =>
@@ -316,7 +311,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** would it be more efficient to use a path like in the above functions ? *)
 
-  Fixpoint choose (m: t) :=
+  Fixpoint choose (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r => if o then Some 1 else
@@ -326,7 +321,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint min_elt (m: t) :=
+  Fixpoint min_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -336,7 +331,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint max_elt (m: t) :=
+  Fixpoint max_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -414,10 +409,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     case o; trivial.
     destruct l; trivial.
     destruct r; trivial.
-    symmetry. destruct x.
-      apply mem_Leaf.
-      apply mem_Leaf.
-      reflexivity.
+    destruct x; reflexivity.
   Qed.
   Local Opaque node.
 
@@ -427,7 +419,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold Empty, In.
     induction s as [|l IHl o r IHr]; simpl.
-      setoid_rewrite mem_Leaf. firstorder.
+      firstorder.
       rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr.
       destruct o; simpl; split.
         intuition discriminate.
@@ -813,7 +805,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        rewrite <- andb_lazy_alt. apply andb_true_iff.
   Qed.
 
-  Lemma filter_spec: forall s x f, compat_bool E.eq f ->
+  Lemma filter_spec: forall s x f, @compat_bool elt E.eq f ->
     (In x (filter f s) <-> In x s /\ f x = true).
   Proof. intros. apply xfilter_spec. Qed.
 
@@ -824,7 +816,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold For_all, In. intro f.
     induction s as [|l IHl o r IHr]; intros i; simpl.
-     setoid_rewrite mem_Leaf. intuition discriminate.
+    intuition discriminate.
      rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -838,7 +830,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         apply H. assumption.
   Qed.
 
-  Lemma for_all_spec: forall s f, compat_bool E.eq f ->
+  Lemma for_all_spec: forall s f, @compat_bool elt E.eq f ->
     (for_all f s = true <-> For_all (fun x => f x = true) s).
   Proof. intros. apply xforall_spec. Qed.
 
@@ -849,7 +841,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold Exists, In. intro f.
     induction s as [|l IHl o r IHr]; intros i; simpl.
-     setoid_rewrite mem_Leaf. firstorder.
+     firstorder.
      rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -860,7 +852,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        intros [[x|x|] H]; eauto.
   Qed.
 
-  Lemma exists_spec : forall s f, compat_bool E.eq f ->
+  Lemma exists_spec : forall s f, @compat_bool elt E.eq f ->
     (exists_ f s = true <-> Exists (fun x => f x = true) s).
   Proof. intros. apply xexists_spec. Qed.
 
@@ -876,11 +868,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o; simpl; rewrite IHl, IHr; reflexivity.
   Qed.
 
-  Lemma partition_spec1 : forall s f, compat_bool E.eq f ->
+  Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f ->
       Equal (fst (partition f s)) (filter f s).
   Proof. intros. rewrite partition_filter. reflexivity. Qed.
 
-  Lemma partition_spec2 : forall s f, compat_bool E.eq f ->
+  Lemma partition_spec2 : forall s f, @compat_bool elt E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
   Proof. intros. rewrite partition_filter. reflexivity. Qed.
 
@@ -897,7 +889,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; simpl.
       intros. split; intro H.
         left. assumption.
-        destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_spec Hx').
+        destruct H as [H|[x [Hx Hx']]]. assumption. discriminate.
 
       intros j acc y. case o.
         rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split.
@@ -1087,7 +1079,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
           destruct (min_elt r).
             injection H. intros <-. clear H.
             destruct y as [z|z|].
-              apply (IHr p z); trivial.
+              apply (IHr e z); trivial.
               elim (Hp _ H').
               discriminate.
             discriminate.
@@ -1141,7 +1133,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
             injection H. intros <-. clear H.
             destruct y as [z|z|].
               elim (Hp _ H').
-              apply (IHl p z); trivial.
+              apply (IHl e z); trivial.
               discriminate.
             discriminate.
   Qed.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b838495f..751d4f35 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -31,13 +31,12 @@ Additional suggested reading:
 *)
 
 Require MSetGenTree.
-Require Import Bool List BinPos Pnat Setoid SetoidList NPeano.
+Require Import Bool List BinPos Pnat Setoid SetoidList PeanoNat.
 Local Open Scope list_scope.
 
 (* For nicer extraction, we create induction principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** An extra function not (yet?) in MSetInterface.S *)
 
@@ -399,7 +398,7 @@ Definition skip_black t :=
 Fixpoint compare_height (s1x s1 s2 s2x: tree) : comparison :=
  match skip_red s1x, skip_red s1, skip_red s2, skip_red s2x with
  | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
-   compare_height (skip_black s2x') s1' s2' (skip_black s2x')
+   compare_height (skip_black s1x') s1' s2' (skip_black s2x')
  | _, Leaf, _, Node _ _ _ _ => Lt
  | Node _ _ _ _, _, Leaf, _ => Gt
  | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Leaf =>
@@ -452,7 +451,7 @@ Local Notation Bk := (Node Black).
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
@@ -980,7 +979,7 @@ Proof.
   { transitivity size; trivial. subst. auto with arith. }
  destruct acc1 as [|x acc1].
   { exfalso. revert LE. apply Nat.lt_nge. subst.
-    rewrite <- app_nil_end, <- elements_cardinal; auto with arith. }
+    rewrite app_nil_r, <- elements_cardinal; auto with arith. }
  specialize (Hg acc1).
  destruct (g acc1) as (t2,acc2).
  destruct Hg as (Hg1,Hg2).
@@ -988,7 +987,7 @@ Proof.
     rewrite app_length, <- elements_cardinal. simpl.
     rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
     apply Nat.add_le_mono_l. }
- simpl. rewrite elements_node, app_ass. now subst.
+ rewrite elements_node, app_ass. now subst.
 Qed.
 
 Lemma treeify_aux_spec n (p:bool) :
@@ -1013,7 +1012,7 @@ Qed.
 Lemma plength_aux_spec l p :
   Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p.
 Proof.
- revert p. induction l; simpl; trivial.
+ revert p. induction l; trivial. simpl plength_aux.
  intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r.
 Qed.
 
@@ -1059,7 +1058,7 @@ Lemma filter_aux_elements s f acc :
  filter_aux f s acc = List.filter f (elements s) ++ acc.
 Proof.
  revert acc.
- induction s as [|c l IHl x r IHr]; simpl; trivial.
+ induction s as [|c l IHl x r IHr]; trivial.
  intros acc.
  rewrite elements_node, filter_app. simpl.
  destruct (f x); now rewrite IHl, IHr, app_ass.
@@ -1197,7 +1196,7 @@ Lemma INV_rev l1 l2 acc :
 Proof.
  intros. rewrite rev_append_rev.
  apply SortA_app with X.eq; eauto with *.
- intros x y. inA. eapply l1_lt_acc; eauto.
+ intros x y. inA. eapply @l1_lt_acc; eauto.
 Qed.
 
 (** ** union *)
@@ -1567,7 +1566,7 @@ Proof.
 Qed.
 
 Lemma maxdepth_upperbound s : Rbt s ->
- maxdepth s <= 2 * log2 (S (cardinal s)).
+ maxdepth s <= 2 * Nat.log2 (S (cardinal s)).
 Proof.
  intros (n,H).
  eapply Nat.le_trans; [eapply rb_maxdepth; eauto|].
@@ -1582,7 +1581,7 @@ Proof.
 Qed.
 
 Lemma maxdepth_lowerbound s : s<>Leaf ->
- log2 (cardinal s) < maxdepth s.
+ Nat.log2 (cardinal s) < maxdepth s.
 Proof.
  apply maxdepth_log_cardinal.
 Qed.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index fd4114cd..372acd56 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -56,8 +56,8 @@ Module Ops (X: DecidableType) <: WOps X.
         if X.eq_dec x y then l else y :: remove x l
     end.
 
-  Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
-    fold_left (flip f) s i.
+  Definition fold (B : Type) (f : elt -> B -> B) : t -> B -> B :=
+    fold_left (flip f).
 
   Definition union (s : t) : t -> t := fold add s.
 
@@ -118,16 +118,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Notation In := (InA X.eq).
 
   (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
+  Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
+  Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+  Hint Resolve eqr eqtrans.
+  Hint Immediate eqsym.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
   Hint Unfold Ok.
-  Hint Resolve @ok.
+  Hint Resolve ok.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
 
@@ -215,10 +217,10 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Proof.
   induction s; simpl; intros.
   intuition; inv; auto.
-  destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition.
+  destruct X.eq_dec as [|Hnot]; inv; rewrite !InA_cons, ?IHs; intuition.
   elim H. setoid_replace a with y; eauto.
   elim H3. setoid_replace x with y; eauto.
-  elim n. eauto.
+  elim Hnot. eauto.
   Qed.
 
   Global Instance remove_ok s x `(Ok s) : Ok (remove x s).