5 files changed, 98 insertions, 98 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 5d34a4bf5..bee922c6f 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -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.
 
@@ -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.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 85b7242b5..0e3b5cef1 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.
@@ -678,7 +672,7 @@ Qed.
 Add Parametric Morphism elt : (@Empty elt)
  with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros m m' Hm; intuition.
+unfold Empty; intros m m' Hm. split; intros; intro. 
 rewrite <-Hm in H0; eapply H, H0.
 rewrite Hm in H0; eapply H, H0.
 Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index f15ab222c..64d5b1c9a 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -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.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 792b88717..253800a45 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -8,7 +8,7 @@
 
 (** * 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.
@@ -69,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
@@ -93,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 =>
@@ -104,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 =>
@@ -115,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
@@ -131,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
@@ -163,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 =>
@@ -190,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 : t A) = 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.
@@ -236,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;
@@ -265,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.
@@ -282,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
@@ -298,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.
@@ -306,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.
@@ -322,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.
@@ -337,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.
@@ -353,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.
@@ -368,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).
@@ -381,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).
@@ -394,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.
@@ -409,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.
@@ -424,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.
@@ -458,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.
@@ -479,18 +479,18 @@ 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 Instance eqk_equiv : Equivalence eq_key := _.
   Global Instance eqke_equiv : Equivalence eq_key_elt := _.
@@ -715,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.
@@ -727,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)))
@@ -746,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.
@@ -756,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.
@@ -820,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.
@@ -832,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.
@@ -848,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.
@@ -896,9 +896,9 @@ 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
         | Node l (Some x) r =>
@@ -1070,7 +1070,7 @@ 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.
@@ -1079,7 +1079,7 @@ Module PositiveMapAdditionalFacts.
 
    (* 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.
@@ -1118,4 +1118,3 @@ Module PositiveMapAdditionalFacts.
   Qed.
 
 End PositiveMapAdditionalFacts.
-
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 670d09154..efd49f54e 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -27,7 +27,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
 
-  Definition elt := positive.
+  Definition elt := positive : Type.
 
   Inductive tree :=
     | Leaf : tree
@@ -35,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
@@ -45,7 +45,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     | Node l b r => negb b &&& is_empty l &&& is_empty r
    end.
 
+<<<<<<< HEAD
   Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
+=======
+  Fixpoint mem (i : elt) (m : t) : bool :=
+>>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
     match m with
     | Leaf => false
     | Node l o r =>
@@ -56,7 +60,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
@@ -76,13 +80,17 @@ 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.
 
+<<<<<<< HEAD
   Fixpoint remove (i : positive) (m : t) {struct m} : t :=
+=======
+  Fixpoint remove (i : elt) (m : t) : t :=
+>>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -93,7 +101,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 =>
@@ -103,7 +111,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 =>
@@ -113,7 +121,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 =>
@@ -145,7 +153,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
@@ -156,8 +164,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
@@ -165,7 +173,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 =>
@@ -179,9 +187,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 =>
@@ -189,21 +197,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 =>
@@ -221,7 +229,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)
@@ -245,7 +253,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
@@ -255,7 +263,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 =>
@@ -265,7 +273,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 =>
@@ -750,7 +758,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.
@@ -798,15 +806,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.
 
@@ -831,11 +839,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.
 
@@ -858,11 +866,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.
 
@@ -878,11 +886,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.
 
@@ -990,7 +998,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.
 
@@ -1101,7 +1109,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.
@@ -1155,7 +1163,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.