Imported Upstream version 8.5~beta1+dfsg

13 files changed, 233 insertions, 230 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c68216e6..c9e5b8dd 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
    | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
   end.
 
-(** then [elements] is an instanciation with an empty [acc] *)
+(** then [elements] is an instantiation with an empty [acc] *)
 
 Definition elements := elements_aux nil.
 
@@ -342,7 +342,7 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
 
 Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _   => Leaf _
    | Node l x d r h => Node (map f l) x (f d) (map f r) h
   end.
 
@@ -350,7 +350,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
 
 Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
   end.
 
@@ -359,7 +359,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
 Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
   : t elt' :=
   match m with
-   | Leaf => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h =>
       match f x d with
        | Some d' => join (map_option f l) x d' (map_option f r)
@@ -370,7 +370,7 @@ Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
 (** * Optimized map2
 
   Suggestion by B. Gregoire: a [map2] function with specialized
-  arguments allowing to bypass some tree traversal. Instead of one
+  arguments that allows bypassing some tree traversal. Instead of one
   [f0] of type [key -> option elt -> option elt' -> option elt''],
   we ask here for:
   - [f] which is a specialisation of [f0] when first option isn't [None]
@@ -389,8 +389,8 @@ Variable mapr : t elt' -> t elt''.
 
 Fixpoint map2_opt m1 m2 :=
  match m1, m2 with
-  | Leaf, _ => mapr m2
-  | _, Leaf => mapl m1
+  | Leaf _, _ => mapr m2
+  | _, Leaf _ => mapl m1
   | Node l1 x1 d1 r1 h1, _ =>
      let (l2',o2,r2') := split x1 m2 in
      match f x1 d1 o2 with
@@ -534,7 +534,7 @@ Ltac order := match goal with
  | _ => MX.order
 end.
 
-Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
+Ltac intuition_in := repeat (intuition; inv In; inv MapsTo).
 
 (* Function/Functional Scheme can't deal with internal fix.
    Let's do its job by hand: *)
@@ -1247,11 +1247,11 @@ Proof.
  intros m1 m2; functional induction (concat m1 m2); intros; auto;
  try factornode _x _x0 _x1 _x2 _x3 as m1.
  apply join_bst; auto.
- change (bst (m2',xd)#1); rewrite <-e1; eauto.
+ change (bst (m2',xd)#1). rewrite <-e1; eauto.
  intros y Hy.
  apply H1; auto.
  rewrite remove_min_in, e1; simpl; auto.
- change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto.
+ change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
 Hint Resolve concat_bst.
 
@@ -1270,10 +1270,10 @@ Proof.
 
  inv bst.
  rewrite H2, join_find; auto; clear H2.
- simpl; destruct X.compare; simpl; auto.
+ simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto.
  destruct (find y m2'); auto.
  symmetry; rewrite not_find_iff; auto; intro.
- apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto.
+ apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto.
 
  intros z Hz; apply H1; auto; rewrite H3; auto.
 Qed.
@@ -1367,7 +1367,7 @@ Proof.
  induction s; simpl; intros; auto.
  rewrite IHs1, IHs2.
  unfold elements; simpl.
- rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto.
+ rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto.
 Qed.
 
 Lemma elements_node :
@@ -1376,7 +1376,7 @@ Lemma elements_node :
  elements (Node t1 x e t2 z) ++ l.
 Proof.
  unfold elements; simpl; intros.
- rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
+ rewrite !elements_app, !app_nil_r, !app_ass; auto.
 Qed.
 
 (** * Fold *)
@@ -1424,7 +1424,7 @@ Qed.
     i.e. the list of elements actually compared *)
 
 Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
-  | End => nil
+  | End _ => nil
   | More x e t r => (x,e) :: elements t ++ flatten_e r
  end.
 
@@ -1433,14 +1433,14 @@ Lemma flatten_e_elements :
  elements l ++ flatten_e (More x d r e) =
  elements (Node l x d r z) ++ flatten_e e.
 Proof.
- intros; simpl; apply elements_node.
+ intros; apply elements_node.
 Qed.
 
 Lemma cons_1 : forall (s:t elt) e,
   flatten_e (cons s e) = elements s ++ flatten_e e.
 Proof.
-  induction s; simpl; auto; intros.
-  rewrite IHs1; apply flatten_e_elements; auto.
+  induction s; auto; intros.
+  simpl flatten_e; rewrite IHs1; apply flatten_e_elements; auto.
 Qed.
 
 (** Proof of correction for the comparison *)
@@ -1478,7 +1478,7 @@ Lemma equal_cont_IfEq : forall m1 cont e2 l,
   (forall e, IfEq (cont e) l (flatten_e e)) ->
   IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).
 Proof.
- induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+ induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto.
  rewrite <- elements_node; simpl.
  apply Hl1; auto.
  clear e2; intros [|x2 d2 r2 e2].
@@ -1491,9 +1491,9 @@ Lemma equal_IfEq : forall (m1 m2:t elt),
   IfEq (equal cmp m1 m2) (elements m1) (elements m2).
 Proof.
  intros; unfold equal.
- rewrite (app_nil_end (elements m1)).
+ rewrite <- (app_nil_r (elements m1)).
  replace (elements m2) with (flatten_e (cons m2 (End _)))
-  by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto).
+  by (rewrite cons_1; simpl; rewrite app_nil_r; auto).
  apply equal_cont_IfEq.
  intros.
  apply equal_end_IfEq; auto.
@@ -1622,8 +1622,8 @@ Lemma map_option_find : forall (m:t elt)(x:key),
 Proof.
 intros m; functional induction (map_option f m); simpl; auto; intros;
  inv bst; rewrite join_find || rewrite concat_find; auto; simpl;
- try destruct X.compare; simpl; auto.
-rewrite (f_compat d e); auto.
+ try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto.
+rewrite (f_compat d Heq); auto.
 intros y H;
  destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
 intros y H;
@@ -1631,7 +1631,7 @@ intros y H;
 
 rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto.
 rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto.
-rewrite (f_compat d e); auto.
+rewrite (f_compat d Heq); auto.
 rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto.
  destruct (find x0 (map_option f r)); auto.
 
@@ -1930,7 +1930,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma Equivb_Equivb : forall cmp m m',
   Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
  Proof.
- intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
+ intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. 
  generalize (H0 k); do 2 rewrite In_alt; intuition.
  generalize (H0 k); do 2 rewrite In_alt; intuition.
  generalize (H0 k); do 2 rewrite <- In_alt; intuition.
@@ -2016,7 +2016,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
    match e2 with
-    | R.End => Gt
+    | R.End _ => Gt
     | R.More x2 d2 r2 e2 =>
        match X.compare x1 x2 with
         | EQ _ => match D.compare d1 d2 with
@@ -2033,7 +2033,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
    match s1 with
-    | R.Leaf => cont e2
+    | R.Leaf _ => cont e2
     | R.Node l1 x1 d1 r1 _ =>
        compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
    end.
@@ -2041,7 +2041,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   (** Initial continuation *)
 
   Definition compare_end (e2:R.enumeration D.t) :=
-   match e2 with R.End => Eq | _ => Lt end.
+   match e2 with R.End _ => Eq | _ => Lt end.
 
   (** The complete comparison *)
 
@@ -2084,7 +2084,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    (forall e, Cmp (cont e) l (P.flatten_e e)) ->
    Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).
   Proof.
-   induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+   induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto.
    rewrite <- P.elements_node; simpl.
    apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2].
    simpl; auto.
@@ -2096,9 +2096,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2).
   Proof.
    intros; unfold compare_pure.
-   rewrite (app_nil_end (R.elements s1)).
+   rewrite <- (app_nil_r (R.elements s1)).
    replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by
-    (rewrite P.cons_1; simpl; rewrite <- app_nil_end; auto).
+    (rewrite P.cons_1; simpl; rewrite app_nil_r; auto).
    auto using compare_cont_Cmp, compare_end_Cmp.
   Qed.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 0c1448c9..8c6f4b64 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -437,12 +437,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
 destruct (eq_dec x y); auto.
 Qed.
 
-Definition option_map (A B:Type)(f:A->B)(o:option A) : option B :=
- match o with
-  | Some a => Some (f a)
-  | None => None
- end.
-
 Lemma map_o : forall m x (f:elt->elt'),
  find x (map f m) = option_map f (find x m).
 Proof.
@@ -519,7 +513,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, elements_mapsto_iff.
 unfold eqb.
-rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto.
+rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto.
 Qed.
 
 Lemma elements_b : forall m x,
@@ -678,9 +672,9 @@ Qed.
 Add Parametric Morphism elt : (@Empty elt)
  with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros m m' Hm; intuition.
-rewrite <-Hm in H0; eauto.
-rewrite Hm in H0; eauto.
+unfold Empty; intros m m' Hm. split; intros; intro. 
+rewrite <-Hm in H0; eapply H, H0.
+rewrite Hm in H0; eapply H, H0.
 Qed.
 
 Add Parametric Morphism elt : (@is_empty elt)
@@ -708,18 +702,18 @@ Add Parametric Morphism elt : (@add elt)
  with signature E.eq ==> eq ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
-rewrite add_o, add_o; do 2 destruct eq_dec; auto.
-elim n; rewrite <-Hk; auto.
-elim n; rewrite Hk; auto.
+rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto.
+elim Hnot; rewrite <-Hk; auto.
+elim Hnot; rewrite Hk; auto.
 Qed.
 
 Add Parametric Morphism elt : (@remove elt)
  with signature E.eq ==> Equal ==> Equal as remove_m.
 Proof.
 intros k k' Hk m m' Hm y.
-rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
-elim n; rewrite <-Hk; auto.
-elim n; rewrite Hk; auto.
+rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto.
+elim Hnot; rewrite <-Hk; auto.
+elim Hnot; rewrite Hk; auto.
 Qed.
 
 Add Parametric Morphism elt elt' : (@map elt elt')
@@ -835,8 +829,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W :=
    fun p => f (fst p) (snd p).
 
-  Definition of_list (l : list (key*elt)) :=
-    List.fold_right (uncurry (@add _)) (empty _) l.
+  Definition of_list :=
+    List.fold_right (uncurry (@add _)) (empty elt).
 
   Definition to_list := elements.
 
@@ -867,7 +861,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
   specialize (IH k Hnodup'); clear Hnodup'.
   rewrite add_o, IH.
-  unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto.
+  unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.
   Qed.
 
   Lemma of_list_2 : forall l, NoDupA eqk l ->
@@ -934,7 +928,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    apply InA_eqke_eqk with k e'; auto.
    rewrite <- of_list_1; auto.
    intro k'. rewrite Hsame, add_o, of_list_1b. simpl.
-   unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto.
+   unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.
    inversion_clear Hdup; auto.
   apply IHl.
    intros; eapply Hstep'; eauto.
@@ -1124,6 +1118,27 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    auto with *.
   Qed.
 
+  Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j ->
+    eqA (fold f m1 i) (fold f m2 j).
+  Proof.
+  intros.
+  rewrite 2 fold_spec_right.
+  assert (NoDupA eqk (rev (elements m1))) by (auto with * ).
+  assert (NoDupA eqk (rev (elements m2))) by (auto with * ).
+  apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke)
+  ; auto with *.
+  - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
+  - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto.
+  - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto.
+    rewrite h'.
+    auto.
+  - rewrite <- NoDupA_altdef; auto.
+  - intros (k,e).
+    rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H;
+      auto with *.
+  Qed.
+
+
   Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
    eqA (fold f m2 i) (f k e (fold f m1 i)).
   Proof.
@@ -1871,14 +1886,9 @@ Module OrdProperties (M:S).
     find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
     add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
-  destruct (E.compare t0 x); intuition.
-  right; split; auto; ME.order.
-  ME.order.
-  elim H.
-  exists e0; apply MapsTo_1 with t0; auto.
-  right; right; split; auto; ME.order.
-  ME.order.
-  right; split; auto; ME.order.
+  destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto.
+  - elim H; exists e0; apply MapsTo_1 with t0; auto.
+  - fold (~E.lt t0 x); auto.
   Qed.
 
   Lemma elements_Add_Above : forall m m' x e,
@@ -1901,7 +1911,7 @@ Module OrdProperties (M:S).
    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
    add_mapsto_iff by (auto with *).
   unfold O.eqke; simpl. intuition.
-  destruct (E.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
   exfalso.
   assert (In t0 m).
    exists e0; auto.
@@ -1930,7 +1940,7 @@ Module OrdProperties (M:S).
     find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
     add_mapsto_iff by (auto with *).
   unfold O.eqke; simpl. intuition.
-  destruct (E.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
   exfalso.
   assert (In t0 m).
    exists e0; auto.
@@ -1986,7 +1996,7 @@ Module OrdProperties (M:S).
   inversion_clear H1; [ | inversion_clear H2; eauto ].
   red in H3; simpl in H3; destruct H3.
   destruct p as (p1,p2).
-  destruct (E.eq_dec p1 x).
+  destruct (E.eq_dec p1 x) as [Heq|Hneq].
   apply ME.lt_eq with p1; auto.
    inversion_clear H2.
    inversion_clear H5.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index e1c60351..a7be3232 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
     match e with
-     | Raw.End => 0%nat
+     | Raw.End _ => 0%nat
      | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
     end.
 
@@ -674,12 +674,14 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition cardinal_e_2 ee :=
    (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.
 
+  Local Unset Keyed Unification.
+
   Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
    { measure cardinal_e_2 ee } : comparison :=
   match ee with
-  | (Raw.End, Raw.End) => Eq
-  | (Raw.End, Raw.More _ _ _ _) => Lt
-  | (Raw.More _ _ _ _, Raw.End) => Gt
+  | (Raw.End _, Raw.End _) => Eq
+  | (Raw.End _, Raw.More _ _ _ _) => Lt
+  | (Raw.More _ _ _ _, Raw.End _) => Gt
   | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
       match X.compare x1 x2 with
       | EQ _ => match D.compare d1 d2 with
@@ -726,7 +728,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   intros.
   assert (H1:=cons_1 m1 (Raw.End _)).
   assert (H2:=cons_1 m2 (Raw.End _)).
-  simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
+  simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2.
   apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _),
                            Raw.cons m2 (Raw.End _))).
   Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index f15ab222..13cb559b 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -403,7 +403,7 @@ Proof.
  apply H1 with k; destruct (X.eq_dec x k); auto.
 
 
- destruct (X.compare x x'); try contradiction; clear y.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y.
  destruct (H0 x).
  assert (In x ((x',e')::l')).
   apply H; auto.
@@ -527,7 +527,7 @@ Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
    | nil => nil
    | (k,e)::m' => (k,f k e) :: mapi f m'
   end.
-
+ 
 End Elt.
 Section Elt2.
 (* A new section is necessary for previous definitions to work
@@ -543,14 +543,13 @@ Proof.
  intros m x e f.
  (* functional induction map elt elt' f m.  *) (* Marche pas ??? *)
  induction m.
- inversion 1.
+ inversion 1. 
 
  destruct a as (x',e').
  simpl.
- inversion_clear 1.
+ inversion_clear 1.  
  constructor 1.
  unfold eqke in *; simpl in *; intuition congruence.
- constructor 2.
  unfold MapsTo in *; auto.
 Qed.
 
@@ -799,7 +798,7 @@ Proof.
  intros.
  simpl.
  destruct a as (k,e); destruct a0 as (k',e').
- destruct (X.compare k k').
+ destruct (X.compare k k') as [Hlt|Heq|Hlt].
  inversion_clear Hm.
  constructor; auto.
  assert (lelistA (ltk (elt:=elt')) (k, e') ((k',e')::m')) by auto.
@@ -868,8 +867,8 @@ Proof.
  induction m'.
  (* m' = nil *)
  intros; destruct a; simpl.
- destruct (X.compare x t0); simpl; auto.
- inversion_clear Hm; clear H0 l Hm' IHm t0.
+ destruct (X.compare x t0) as [Hlt| |Hlt]; simpl; auto.
+ inversion_clear Hm; clear H0 Hlt Hm' IHm t0.
  induction m; simpl; auto.
  inversion_clear H.
  destruct a.
@@ -923,7 +922,7 @@ Proof.
  destruct o; destruct o'; simpl in *; try discriminate; auto.
  destruct a as (k,(oo,oo')); simpl in *.
  inversion_clear H2.
- destruct (X.compare x k); simpl in *.
+ destruct (X.compare x k) as [Hlt|Heq|Hlt]; simpl in *.
  (* x < k *)
  destruct (f' (oo,oo')); simpl.
  elim_comp.
@@ -959,7 +958,7 @@ Proof.
  destruct a as (k,(oo,oo')).
  simpl.
  inversion_clear H2.
- destruct (X.compare x k).
+ destruct (X.compare x k) as [Hlt|Heq|Hlt].
  (* x < k *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
@@ -1208,7 +1207,7 @@ Proof.
  destruct a as (x,e).
  destruct p as (x',e').
  unfold equal; simpl.
- destruct (X.compare x x'); simpl; intuition.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; simpl; intuition.
  unfold cmp at 1.
  MD.elim_comp; clear H; simpl.
  inversion_clear Hl.
@@ -1245,21 +1244,21 @@ Lemma eq_refl : forall m : t, eq m m.
 Proof.
  intros (m,Hm); induction m; unfold eq; simpl; auto.
  destruct a.
- destruct (X.compare t0 t0); auto.
- apply (MapS.Raw.MX.lt_antirefl l); auto.
+ destruct (X.compare t0 t0) as [Hlt|Heq|Hlt]; auto.
+ apply (MapS.Raw.MX.lt_antirefl Hlt); auto.
  split.
  apply D.eq_refl.
  inversion_clear Hm.
  apply (IHm H).
- apply (MapS.Raw.MX.lt_antirefl l); auto.
+ apply (MapS.Raw.MX.lt_antirefl Hlt); auto.
 Qed.
 
-Lemma  eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
+Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
 Proof.
  intros (m,Hm); induction m;
  intros (m', Hm'); destruct m'; unfold eq; simpl;
  try destruct a as (x,e); try destruct p as (x',e'); auto.
- destruct (X.compare x x'); MapS.Raw.MX.elim_comp; intuition.
+ destruct (X.compare x x')  as [Hlt|Heq|Hlt]; MapS.Raw.MX.elim_comp; intuition.
  inversion_clear Hm; inversion_clear Hm'.
  apply (IHm H0 (Build_slist H4)); auto.
 Qed.
@@ -1272,8 +1271,8 @@ Proof.
  try destruct a as (x,e);
  try destruct p as (x',e');
  try destruct p0 as (x'',e''); try contradiction; auto.
- destruct (X.compare x x');
-  destruct (X.compare x' x'');
+ destruct (X.compare x x') as [Hlt|Heq|Hlt];
+  destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt'];
    MapS.Raw.MX.elim_comp; intuition.
  apply D.eq_trans with e'; auto.
  inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3.
@@ -1288,8 +1287,8 @@ Proof.
  try destruct a as (x,e);
  try destruct p as (x',e');
  try destruct p0 as (x'',e''); try contradiction; auto.
- destruct (X.compare x x');
-  destruct (X.compare x' x'');
+ destruct (X.compare x x') as [Hlt|Heq|Hlt];
+  destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt'];
    MapS.Raw.MX.elim_comp; intuition.
  left; apply D.lt_trans with e'; auto.
  left; apply lt_eq with e'; auto.
@@ -1307,7 +1306,7 @@ Proof.
  intros (m2, Hm2); destruct m2; unfold eq, lt; simpl;
  try destruct a as (x,e);
  try destruct p as (x',e'); try contradiction; auto.
- destruct (X.compare x x'); auto.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; auto.
  intuition.
  exact (D.lt_not_eq H0 H1).
  inversion_clear Hm1; inversion_clear Hm2.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c59f7c22..3eac15b0 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -8,13 +8,11 @@
 
 (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
 
-Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
+Require Import Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
 Local Open Scope positive_scope.
-
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** This file is an adaptation to the [FMap] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
@@ -71,7 +69,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Module E:=PositiveOrderedTypeBits.
   Module ME:=KeyOrderedType E.
 
-  Definition key := positive.
+  Definition key := positive : Type. 
 
   Inductive tree (A : Type) :=
     | Leaf : tree A
@@ -84,7 +82,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section A.
   Variable A:Type.
 
-  Arguments Leaf [A].
+  Arguments Leaf {A}.
 
   Definition empty : t A := Leaf.
 
@@ -95,7 +93,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | _ => false
    end.
 
-  Fixpoint find (i : positive) (m : t A) : option A :=
+  Fixpoint find (i : key) (m : t A) : option A :=
     match m with
     | Leaf => None
     | Node l o r =>
@@ -106,7 +104,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint mem (i : positive) (m : t A) : bool :=
+  Fixpoint mem (i : key) (m : t A) : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -117,7 +115,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint add (i : positive) (v : A) (m : t A) : t A :=
+  Fixpoint add (i : key) (v : A) (m : t A) : t A :=
     match m with
     | Leaf =>
         match i with
@@ -133,7 +131,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint remove (i : positive) (m : t A) : t A :=
+  Fixpoint remove (i : key) (m : t A) : t A :=
     match i with
     | xH =>
         match m with
@@ -165,7 +163,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   (** [elements] *)
 
-    Fixpoint xelements (m : t A) (i : positive) : list (positive * A) :=
+    Fixpoint xelements (m : t A) (i : key) : list (key * A) :=
       match m with
       | Leaf => nil
       | Node l None r =>
@@ -192,33 +190,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section CompcertSpec.
 
   Theorem gempty:
-    forall (i: positive), find i empty = None.
+    forall (i: key), find i empty = None.
   Proof.
     destruct i; simpl; auto.
   Qed.
 
   Theorem gss:
-    forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x.
+    forall (i: key) (x: A) (m: t A), find i (add i x m) = Some x.
   Proof.
     induction i; destruct m; simpl; auto.
   Qed.
 
-  Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None.
+  Lemma gleaf : forall (i : key), find i (Leaf : t A) = None.
   Proof. exact gempty. Qed.
 
   Theorem gso:
-    forall (i j: positive) (x: A) (m: t A),
+    forall (i j: key) (x: A) (m: t A),
     i <> j -> find i (add j x m) = find i m.
   Proof.
     induction i; intros; destruct j; destruct m; simpl;
        try rewrite <- (gleaf i); auto; try apply IHi; congruence.
   Qed.
 
-  Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf.
+  Lemma rleaf : forall (i : key), remove i Leaf = Leaf.
   Proof. destruct i; simpl; auto. Qed.
 
   Theorem grs:
-    forall (i: positive) (m: t A), find i (remove i m) = None.
+    forall (i: key) (m: t A), find i (remove i m) = None.
   Proof.
     induction i; destruct m.
      simpl; auto.
@@ -238,7 +236,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Theorem gro:
-    forall (i j: positive) (m: t A),
+    forall (i j: key) (m: t A),
     i <> j -> find i (remove j m) = find i m.
   Proof.
     induction i; intros; destruct j; destruct m;
@@ -267,11 +265,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Lemma xelements_correct:
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       find i m = Some v -> List.In (append j i, v) (xelements m j).
     Proof.
       induction m; intros.
-       rewrite (gleaf i) in H; congruence.
+       rewrite (gleaf i) in H; discriminate. 
        destruct o; destruct i; simpl; simpl in H.
         rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
           apply IHm2; auto.
@@ -284,14 +282,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
   Theorem elements_correct:
-    forall (m: t A) (i: positive) (v: A),
+    forall (m: t A) (i: key) (v: A),
     find i m = Some v -> List.In (i, v) (elements m).
   Proof.
     intros m i v H.
     exact (xelements_correct m i xH H).
   Qed.
 
-  Fixpoint xfind (i j : positive) (m : t A) : option A :=
+  Fixpoint xfind (i j : key) (m : t A) : option A :=
       match i, j with
       | _, xH => find i m
       | xO ii, xO jj => xfind ii jj m
@@ -300,7 +298,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       end.
 
    Lemma xfind_left :
-      forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+      forall (j i : key) (m1 m2 : t A) (o : option A) (v : A),
       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.
@@ -308,7 +306,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ii :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -324,7 +322,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_io :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       ~List.In (xI i, v) (xelements m (xO j)).
     Proof.
       induction m.
@@ -339,7 +337,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oo :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -355,7 +353,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oi :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       ~List.In (xO i, v) (xelements m (xI j)).
     Proof.
       induction m.
@@ -370,7 +368,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ih :
-      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (m1 m2: t A) (o: option A) (i : key) (v: A),
       List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -383,7 +381,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oh :
-      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (m1 m2: t A) (o: option A) (i : key) (v: A),
       List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -396,7 +394,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_hi :
-      forall (m: t A) (i : positive) (v: A),
+      forall (m: t A) (i : key) (v: A),
       ~List.In (xH, v) (xelements m (xI i)).
     Proof.
       induction m; intros.
@@ -411,7 +409,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ho :
-      forall (m: t A) (i : positive) (v: A),
+      forall (m: t A) (i : key) (v: A),
       ~List.In (xH, v) (xelements m (xO i)).
     Proof.
       induction m; intros.
@@ -426,13 +424,13 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma find_xfind_h :
-      forall (m: t A) (i: positive), find i m = xfind i xH m.
+      forall (m: t A) (i: key), find i m = xfind i xH m.
     Proof.
       destruct i; simpl; auto.
     Qed.
 
     Lemma xelements_complete:
-      forall (i j : positive) (m: t A) (v: A),
+      forall (i j : key) (m: t A) (v: A),
       List.In (i, v) (xelements m j) -> xfind i j m = Some v.
     Proof.
       induction i; simpl; intros; destruct j; simpl.
@@ -460,7 +458,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
   Theorem elements_complete:
-    forall (m: t A) (i: positive) (v: A),
+    forall (m: t A) (i: key) (v: A),
     List.In (i, v) (elements m) -> find i m = Some v.
   Proof.
     intros m i v H.
@@ -481,22 +479,22 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   End CompcertSpec.
 
-  Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v.
+  Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v.
 
-  Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m.
+  Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m.
 
-  Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m.
+  Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m.
 
-  Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p').
+  Definition eq_key (p p':key*A) := E.eq (fst p) (fst p').
 
-  Definition eq_key_elt (p p':positive*A) :=
+  Definition eq_key_elt (p p':key*A) :=
           E.eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-  Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
+  Definition lt_key (p p':key*A) := E.lt (fst p) (fst p').
 
-  Global Program Instance eqk_equiv : Equivalence eq_key.
-  Global Program Instance eqke_equiv : Equivalence eq_key_elt.
-  Global Program Instance ltk_strorder : StrictOrder lt_key.
+  Global Instance eqk_equiv : Equivalence eq_key := _.
+  Global Instance eqke_equiv : Equivalence eq_key_elt := _.
+  Global Instance ltk_strorder : StrictOrder lt_key := _.
 
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
@@ -717,8 +715,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Lemma elements_3w : NoDupA eq_key (elements m).
   Proof.
-  change eq_key with (@ME.eqk A).
-  apply ME.Sort_NoDupA; apply elements_3; auto.
+    apply ME.Sort_NoDupA.
+    apply elements_3.
   Qed.
 
   End FMapSpec.
@@ -729,9 +727,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Mapi.
 
-    Variable f : positive -> A -> B.
+    Variable f : key -> A -> B.
 
-    Fixpoint xmapi (m : t A) (i : positive) : t B :=
+    Fixpoint xmapi (m : t A) (i : key) : t B :=
        match m with
         | Leaf => @Leaf B
         | Node l o r => Node (xmapi l (append i (xO xH)))
@@ -748,7 +746,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   End A.
 
   Lemma xgmapi:
-      forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
+      forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A),
       find i (xmapi f m j) = option_map (f (append j i)) (find i m).
   Proof.
   induction i; intros; destruct m; simpl; auto.
@@ -758,7 +756,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Theorem gmapi:
-    forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
+    forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A),
     find i (mapi f m) = option_map (f i) (find i m).
   Proof.
   intros.
@@ -814,7 +812,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Variable A B C : Type.
   Variable f : option A -> option B -> option C.
 
-  Arguments Leaf [A].
+  Arguments Leaf {A}.
 
   Fixpoint xmap2_l (m : t A) : t C :=
       match m with
@@ -822,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r)
       end.
 
-  Lemma xgmap2_l : forall (i : positive) (m : t A),
+  Lemma xgmap2_l : forall (i : key) (m : t A),
           f None None = None -> find i (xmap2_l m) = f (find i m) None.
     Proof.
       induction i; intros; destruct m; simpl; auto.
@@ -834,7 +832,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r)
       end.
 
-  Lemma xgmap2_r : forall (i : positive) (m : t B),
+  Lemma xgmap2_r : forall (i : key) (m : t B),
           f None None = None -> find i (xmap2_r m) = f None (find i m).
     Proof.
       induction i; intros; destruct m; simpl; auto.
@@ -850,7 +848,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-    Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B),
+    Lemma gmap2: forall (i: key)(m1:t A)(m2: t B),
       f None None = None ->
       find i (_map2 m1 m2) = f (find i m1) (find i m2).
     Proof.
@@ -898,11 +896,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section Fold.
 
     Variables A B : Type.
-    Variable f : positive -> A -> B -> B.
+    Variable f : key -> A -> B -> B.
 
-    Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
+    Fixpoint xfoldi (m : t A) (v : B) (i : key) :=
       match m with
-        | Leaf => v
+        | Leaf _ => v
         | Node l (Some x) r =>
           xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
         | Node l None r =>
@@ -940,8 +938,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   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
+      | Leaf _, _ => is_empty m2
+      | _, Leaf _ => is_empty m1
       | Node l1 o1 r1, Node l2 o2 r2 =>
            (match o1, o2 with
              | None, None => true
@@ -1072,16 +1070,16 @@ Module PositiveMapAdditionalFacts.
 
   (* Derivable from the Map interface *)
   Theorem gsspec:
-    forall (A:Type)(i j: positive) (x: A) (m: t A),
+    forall (A:Type)(i j: key) (x: A) (m: t A),
     find i (add j x m) = if E.eq_dec i j then Some x else find i m.
   Proof.
     intros.
-    destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
+    destruct (E.eq_dec i j) as [ ->|]; [ apply gss | apply gso; auto ].
   Qed.
 
    (* Not derivable from the Map interface *)
   Theorem gsident:
-    forall (A:Type)(i: positive) (m: t A) (v: A),
+    forall (A:Type)(i: key) (m: t A) (v: A),
     find i m = Some v -> add i v m = m.
   Proof.
     induction i; intros; destruct m; simpl; simpl in H; try congruence.
@@ -1120,4 +1118,3 @@ Module PositiveMapAdditionalFacts.
   Qed.
 
 End PositiveMapAdditionalFacts.
-
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 6c1e8ca8..0f11dd7a 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -146,9 +146,10 @@ Proof.
  induction m; simpl; auto; destruct a; intros.
  inversion_clear Hm.
  rewrite (IHm H1 x x'); auto.
- destruct (X.eq_dec x t0); destruct (X.eq_dec x' t0); trivial.
- elim n; apply X.eq_trans with x; auto.
- elim n; apply X.eq_trans with x'; auto.
+ destruct (X.eq_dec x t0) as [|Hneq]; destruct (X.eq_dec x' t0) as [|?Hneq'];
+   trivial.
+ elim Hneq'; apply X.eq_trans with x; auto.
+ elim Hneq; apply X.eq_trans with x'; auto.
 Qed.
 
 (** * [add] *)
@@ -600,18 +601,18 @@ Definition combine_l (m:t elt)(m':t elt') : t oee' :=
 Definition combine_r (m:t elt)(m':t elt') : t oee' :=
   mapi (fun k e' => (find k m, Some e')) m'.
 
-Definition fold_right_pair (A B C:Type)(f:A->B->C->C)(l:list (A*B))(i:C) :=
-  List.fold_right (fun p => f (fst p) (snd p)) i l.
+Definition fold_right_pair (A B C:Type)(f:A->B->C->C) :=
+  List.fold_right (fun p => f (fst p) (snd p)).
 
 Definition combine (m:t elt)(m':t elt') : t oee' :=
   let l := combine_l m m' in
   let r := combine_r m m' in
-  fold_right_pair (add (elt:=oee')) l r.
+  fold_right_pair (add (elt:=oee')) r l.
 
 Lemma fold_right_pair_NoDup :
   forall l r (Hl: NoDupA (eqk (elt:=oee')) l)
     (Hl: NoDupA (eqk (elt:=oee')) r),
-    NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r).
+    NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) r l).
 Proof.
  induction l; simpl; auto.
  destruct a; simpl; auto.
@@ -733,7 +734,7 @@ Definition option_cons (A:Type)(k:key)(o:option A)(l:list (key*A)) :=
 Definition map2 m m' :=
   let m0 : t oee' := combine m m' in
   let m1 : t (option elt'') := map (fun p => f (fst p) (snd p)) m0 in
-  fold_right_pair (option_cons (A:=elt'')) m1 nil.
+  fold_right_pair (option_cons (A:=elt'')) nil m1.
 
 Lemma map2_NoDup :
   forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'),
@@ -787,14 +788,14 @@ Proof.
  destruct o; destruct o'; simpl in *; try discriminate; auto.
  destruct a as (k,(oo,oo')); simpl in *.
  inversion_clear H2.
- destruct (X.eq_dec x k); simpl in *.
+ destruct (X.eq_dec x k) as [|Hneq]; simpl in *.
  (* x = k *)
  assert (at_least_one_then_f o o' = f oo oo').
   destruct o; destruct o'; simpl in *; inversion_clear H; auto.
  rewrite H2.
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); try contradict n; auto.
+ destruct (X.eq_dec x k) as [|Hneq]; try contradict Hneq; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  case_eq (find x m0); intros; auto.
  elim H0.
@@ -804,7 +805,7 @@ Proof.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ contradict n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict Hneq; auto | auto].
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
 
@@ -812,13 +813,13 @@ Proof.
  destruct a as (k,(oo,oo')).
  simpl.
  inversion_clear H2.
- destruct (X.eq_dec x k).
+ destruct (X.eq_dec x k) as [|Hneq].
  (* x = k *)
  discriminate.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ contradict n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict Hneq; auto | auto].
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
 Qed.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 1ac544e1..97f140b3 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
 
   Lemma choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _                        => False
      end.
@@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition choose (s : t) : option elt :=
     match choose s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition min_elt (s : t) : option elt :=
     match min_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition max_elt (s : t) : option elt :=
     match max_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -673,24 +673,24 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x (filter f s) -> In x s.
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Lemma filter_2 :
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x (filter f s) -> f x = true.
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Lemma filter_3 :
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Definition for_all (f : elt -> bool) (s : t) : bool :=
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 6b3d86d3..b1769da3 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -283,6 +283,8 @@ Module Update_WSets
 
   Lemma is_empty_spec : is_empty s = true <-> Empty s.
   Proof. intros; symmetry; apply MF.is_empty_iff. Qed.
+  
+  Declare Equivalent Keys In M.In.
 
   Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s.
   Proof. intros. rewrite MF.add_iff. intuition. Qed.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index f64df9fe..ad067eb3 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -15,7 +15,7 @@
 (** This file implements a decision procedure for a certain
     class of propositions involving finite sets.  *)
 
-Require Import Decidable DecidableTypeEx FSetFacts.
+Require Import Decidable Setoid DecidableTypeEx FSetFacts.
 
 (** 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 FSetLogicalFacts.
-    Require Export Decidable.
-    Require Export Setoid.
+    Export Decidable.
+    Export Setoid.
 
     (** ** Lemmas and Tactics About Decidable Propositions *)
 
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ac495c04..f2f4cc2c 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -822,7 +822,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.
+destruct (for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,p); auto.
 elim p;intros.
 exists x;split;auto.
 rewrite <-negb_false_iff; auto.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a0361119..c791f49a 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -497,7 +497,7 @@ Module Type Sdep.
         in the dependent version of [choose], so we leave it separate. *)
   Parameter choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _  => False
      end.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index e5d55ac5..7398c6d6 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -19,20 +19,15 @@
 Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface.
 
 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.
-
 
 Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
 
-  Definition elt := positive.
+  Definition elt := positive : Type.
 
   Inductive tree :=
     | Leaf : tree
@@ -40,9 +35,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
@@ -50,7 +45,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 : elt) (m : t) {struct m} : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -61,7 +56,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint add (i : positive) (m : t) : t :=
+  Fixpoint add (i : elt) (m : t) : t :=
     match m with
     | Leaf =>
         match i with
@@ -81,13 +76,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 : elt) (m : t) {struct m} : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -98,7 +93,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 =>
@@ -108,7 +103,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 =>
@@ -118,7 +113,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 =>
@@ -150,7 +145,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
@@ -161,8 +156,8 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Fold.
 
-    Variables B : Type.
-    Variable f : positive -> B -> B.
+    Variable B : Type.
+    Variable f : elt -> B -> B.
 
     (** the additional argument, [i], records the current path, in
        reverse order (this should be more efficient: we reverse this argument
@@ -170,7 +165,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        we also use this convention in all functions below
      *)
 
-    Fixpoint xfold (m : t) (v : B) (i : positive) :=
+    Fixpoint xfold (m : t) (v : B) (i : elt) :=
       match m with
         | Leaf => v
         | Node l true r =>
@@ -184,9 +179,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Quantifiers.
 
-    Variable f : positive -> bool.
+    Variable f : elt -> bool.
 
-    Fixpoint xforall (m : t) (i : positive) :=
+    Fixpoint xforall (m : t) (i : elt) :=
       match m with
         | Leaf => true
         | Node l o r =>
@@ -194,21 +189,21 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       end.
     Definition for_all m := xforall m 1.
 
-    Fixpoint xexists (m : t) (i : positive) :=
+    Fixpoint xexists (m : t) (i : elt) :=
       match m with
         | Leaf => false
         | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
       end.
     Definition exists_ m := xexists m 1.
 
-    Fixpoint xfilter (m : t) (i : positive) :=
+    Fixpoint xfilter (m : t) (i : elt) : 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 : elt) : t * t :=
       match m with
         | Leaf => (Leaf,Leaf)
         | Node l o r =>
@@ -226,7 +221,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** uses [a] to accumulate values rather than doing a lot of concatenations *)
 
-  Fixpoint xelements (m : t) (i : positive) (a: list positive) :=
+  Fixpoint xelements (m : t) (i : elt) (a: list elt) :=
     match m with
       | Leaf => a
       | Node l false r => xelements l i~0 (xelements r i~1 a)
@@ -250,7 +245,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
@@ -260,7 +255,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 =>
@@ -270,7 +265,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 =>
@@ -311,6 +306,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq := Equal.
+
+  Declare Equivalent Keys Equal eq.
+
   Definition lt m m' := compare_fun m m' = Lt.
 
   (** Specification of [In] *)
@@ -355,10 +353,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.
+    now destruct x.
   Qed.
   Local Opaque node.
 
@@ -367,8 +362,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Lemma is_empty_spec: forall s, Empty s <-> is_empty s = true.
   Proof.
     unfold Empty, In.
-    induction s as [|l IHl o r IHr]; simpl.
-      setoid_rewrite mem_Leaf. firstorder.
+    induction s as [|l IHl o r IHr]; simpl. now split.
       rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr.
       destruct o; simpl; split.
         intro H. elim (H 1). reflexivity.
@@ -759,7 +753,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof. intros. rewrite diff_spec. split; assumption. Qed.
 
   (** Specification of [fold] *)
-
+  
   Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
@@ -807,15 +801,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        rewrite <- andb_lazy_alt. apply andb_true_iff.
   Qed.
 
-  Lemma filter_1 : forall s x f, compat_bool E.eq f ->
+  Lemma filter_1 : forall s x f, @compat_bool elt E.eq f ->
     In x (filter f s) -> In x s.
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
-  Lemma filter_2 : forall s x f, compat_bool E.eq f ->
+  Lemma filter_2 : forall s x f, @compat_bool elt E.eq f ->
     In x (filter f s) -> f x = true.
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
-  Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s ->
+  Lemma filter_3 : forall s x f, @compat_bool elt E.eq f -> In x s ->
     f x = true -> In x (filter f s).
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
@@ -826,8 +820,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.
   Proof.
     unfold For_all, In. intro f.
-    induction s as [|l IHl o r IHr]; intros i; simpl.
-     setoid_rewrite mem_Leaf. intuition discriminate.
+    induction s as [|l IHl o r IHr]; intros i; simpl. now split.
      rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -841,11 +834,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         apply H. assumption.
   Qed.
 
-  Lemma for_all_1 : forall s f, compat_bool E.eq f ->
+  Lemma for_all_1 : forall s f, @compat_bool elt E.eq f ->
     For_all (fun x => f x = true) s -> for_all f s = true.
   Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
 
-  Lemma for_all_2 : forall s f, compat_bool E.eq f ->
+  Lemma for_all_2 : forall s f, @compat_bool elt E.eq f ->
     for_all f s = true -> For_all (fun x => f x = true) s.
   Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
 
@@ -857,7 +850,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.
+    split; [ discriminate | now intros  [ _ [? _]]].
      rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -868,11 +861,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        intros [[x|x|] H]; eauto.
   Qed.
 
-  Lemma exists_1 : forall s f, compat_bool E.eq f ->
+  Lemma exists_1 : forall s f, @compat_bool elt E.eq f ->
       Exists (fun x => f x = true) s -> exists_ f s = true.
   Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
 
-  Lemma exists_2 : forall s f, compat_bool E.eq f ->
+  Lemma exists_2 : forall s f, @compat_bool elt E.eq f ->
       exists_ f s = true -> Exists (fun x => f x = true) s.
   Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
 
@@ -888,11 +881,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o; simpl; rewrite IHl, IHr; reflexivity.
   Qed.
 
-  Lemma partition_1 : forall s f, compat_bool E.eq f ->
+  Lemma partition_1 : forall s f, @compat_bool elt E.eq f ->
       Equal (fst (partition f s)) (filter f s).
   Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
 
-  Lemma partition_2 : forall s f, compat_bool E.eq f ->
+  Lemma partition_2 : 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. apply eq_refl. Qed.
 
@@ -909,7 +902,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_1 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.
@@ -1000,7 +993,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       constructor.
        intros x H. apply E.lt_not_eq in H. apply H. reflexivity.
        intro. apply E.lt_trans.
-      intros ? ? <- ? ? <-. reflexivity.
+     solve_proper.
       apply elements_3.
   Qed.
 
@@ -1111,7 +1104,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.
@@ -1165,7 +1158,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/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index d53ce0c8..25b042ca 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -995,8 +995,7 @@ Module OrdProperties (M:S).
    leb_1, gtb_1, (H0 a) by auto with *.
   intuition.
   destruct (E.compare a x); intuition.
-  right; right; split; auto with *.
-  ME.order.
+  fold (~E.lt a x); auto with *.
   Qed.
 
   Definition Above x s := forall y, In y s -> E.lt y x.