1 files changed, 42 insertions, 34 deletions

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.