migration from Set to Type of FSet/FMap + some dependencies...

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

11 files changed, 112 insertions, 112 deletions

diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 351a7c7d7d..bcdc4a7bf4 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -18,7 +18,7 @@ Require Import Map.
 
 Section Dom.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Fixpoint MapDomRestrTo (m:Map A) : Map B -> Map A :=
     match m with
@@ -229,7 +229,7 @@ End Dom.
 
 Section InDom.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma in_dom_restrto :
    forall (m:Map A) (m':Map B) (a:ad),
@@ -259,7 +259,7 @@ Definition FSet := Map unit.
 
 Section FSetDefs.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Definition in_FSet : ad -> FSet -> bool := in_dom unit.
 
diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v
index f8cd372a42..7f818aab78 100644
--- a/theories/IntMap/Lsort.v
+++ b/theories/IntMap/Lsort.v
@@ -19,7 +19,7 @@ Require Import Mapiter.
 
 Section LSort.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Fixpoint alist_sorted (l:alist A) : bool :=
     match l with
@@ -90,7 +90,7 @@ Section LSort.
   Qed.
 
   Lemma app_length :
-   forall (C:Set) (l l':list C), length (l ++ l') = length l + length l'.
+   forall (C:Type) (l l':list C), length (l ++ l') = length l + length l'.
   Proof.
     simple induction l. trivial.
     intros. simpl in |- *. rewrite (H l'). reflexivity.
@@ -172,7 +172,7 @@ Section LSort.
     simple induction l. intros. elim (le_Sn_O _ H).
     intro r. elim r. intros a y l0 H. simple induction n. simpl in |- *. intro. split with y.
     rewrite (Neqb_correct a). reflexivity.
-    intros. elim (H _ (le_S_n _ _ H1)). intros y0 H2.
+    intros. elim (H _ (le_S_n _ _ H0)). intros y0 H2.
     elim (sumbool_of_bool (Neqb a (alist_nth_ad n0 l0))). intro H3. split with y.
     rewrite (Neqb_complete _ _ H3). simpl in |- *. rewrite (Neqb_correct (alist_nth_ad n0 l0)).
     reflexivity.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index 6b914264f0..96c89691dc 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -25,9 +25,9 @@ Definition ad := N.
 Section MapDefs.
 
 (** We now define maps from ad to A. *)
-  Variable A : Set.  
+  Variable A : Type.  
 
-  Inductive Map : Set :=
+  Inductive Map :=
     | M0 : Map
     | M1 : ad -> A -> Map
     | M2 : Map -> Map -> Map.
diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v
index 0343e9e947..6fced32856 100644
--- a/theories/IntMap/Mapaxioms.v
+++ b/theories/IntMap/Mapaxioms.v
@@ -17,7 +17,7 @@ Require Import Fset.
 
 Section MapAxioms.
 
-  Variables A B C : Set.
+  Variables A B C : Type.
 
   Lemma eqm_sym : forall f f':ad -> option A, eqm A f f' -> eqm A f' f.
   Proof.
@@ -574,7 +574,7 @@ Section MapAxioms.
 End MapAxioms.
 
 Lemma MapDomRestrTo_ext :
- forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A) 
+ forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A) 
    (m'2:Map B),
    eqmap A m1 m'1 ->
    eqmap B m2 m'2 ->
@@ -585,7 +585,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrTo_ext_l :
- forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A),
+ forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A),
    eqmap A m1 m'1 ->
    eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m2).
 Proof.
@@ -593,7 +593,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrTo_ext_r :
- forall (A B:Set) (m1:Map A) (m2 m'2:Map B),
+ forall (A B:Type) (m1:Map A) (m2 m'2:Map B),
    eqmap B m2 m'2 ->
    eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m1 m'2).
 Proof.
@@ -601,7 +601,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrBy_ext :
- forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A) 
+ forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A) 
    (m'2:Map B),
    eqmap A m1 m'1 ->
    eqmap B m2 m'2 ->
@@ -612,7 +612,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrBy_ext_l :
- forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A),
+ forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A),
    eqmap A m1 m'1 ->
    eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m2).
 Proof.
@@ -620,7 +620,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrBy_ext_r :
- forall (A B:Set) (m1:Map A) (m2 m'2:Map B),
+ forall (A B:Type) (m1:Map A) (m2 m'2:Map B),
    eqmap B m2 m'2 ->
    eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m1 m'2).
 Proof.
@@ -628,7 +628,7 @@ Proof.
 Qed.
 
 Lemma MapDomRestrBy_m_m :
- forall (A:Set) (m:Map A),
+ forall (A:Type) (m:Map A),
    eqmap A (MapDomRestrBy A unit m (MapDom A m)) (M0 A).
 Proof.
   intros. apply eqmap_trans with (m' := MapDomRestrBy A A m m). apply eqmap_sym.
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index d6a9aad477..8eff8c31df 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -23,7 +23,7 @@ Require Import Mapcanon.
 
 Section MapC.
 
-  Variables A B C : Set.
+  Variables A B C : Type.
 
   Lemma MapPut_as_Merge_c :
    forall m:Map A,
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index 0b922864f0..794ecb12c3 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -24,7 +24,7 @@ Require Import Mapcard.
 
 Section MapCanon.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Inductive mapcanon : Map A -> Prop :=
     | M0_canon : mapcanon (M0 A)
@@ -277,7 +277,7 @@ Section MapCanon.
     exact (mapcanon_M2_2 _ _ H4).
   Qed.
 
-  Variable B : Set.
+  Variable B : Type.
 
   Lemma MapDomRestrTo_canon :
    forall m:Map A,
@@ -337,7 +337,7 @@ End MapCanon.
 
 Section FSetCanon.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Lemma MapDom_canon :
    forall m:Map A, mapcanon A m -> mapcanon unit (MapDom A m).
@@ -354,7 +354,7 @@ End FSetCanon.
 
 Section MapFoldCanon.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapFold_canon_1 :
    forall m0:Map B,
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index 399fc0c537..26ead03ccb 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -24,7 +24,7 @@ Require Import Peano_dec.
 
 Section MapCard.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapCard_M0 : MapCard A (M0 A) = 0.
   Proof.
@@ -55,10 +55,10 @@ Section MapCard.
     reflexivity.
     intro H0. rewrite H0 in H. discriminate H.
     intros. elim (sumbool_of_bool (Nbit0 a)). intro H2.
-    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. elim (H0 (Ndiv2 a) y H1). intros n H3.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H. elim (X0 (Ndiv2 a) y H). intros n H3.
     simpl in |- *. rewrite H3. split with (MapCard A m0 + n).
     rewrite <- (plus_Snm_nSm (MapCard A m0) n). reflexivity.
-    intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. elim (H (Ndiv2 a) y H1).
+    intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H. elim (X (Ndiv2 a) y H).
     intros n H3. simpl in |- *. rewrite H3. split with (n + MapCard A m1). reflexivity.
   Qed.
 
@@ -68,11 +68,11 @@ Section MapCard.
   Proof.
     simple induction m. intro. discriminate H.
     intros a y H. split with a. split with y. apply M1_semantics_1.
-    intros. simpl in H1. elim (plus_is_one (MapCard A m0) (MapCard A m1) H1).
-    intro H2. elim H2. intros. elim (H0 H4). intros a H5. split with (Ndouble_plus_one a).
+    intros. simpl in H. elim (plus_is_one (MapCard A m0) (MapCard A m1) H).
+    intro H2. elim H2. intros H3 H4. elim (X0 H4). intros a H5. split with (Ndouble_plus_one a).
     rewrite (MapGet_M2_bit_0_1 A _ (Ndouble_plus_one_bit0 a) m0 m1).
     rewrite Ndouble_plus_one_div2. exact H5.
-    intro H2. elim H2. intros. elim (H H3). intros a H5. split with (Ndouble a).
+    intro H2. elim H2. intros H3 H4. elim (X H3). intros a H5. split with (Ndouble a).
     rewrite (MapGet_M2_bit_0_0 A _ (Ndouble_bit0 a) m0 m1).
     rewrite Ndouble_div2. exact H5.
   Qed.
@@ -116,7 +116,7 @@ Section MapCard.
   Qed.
 
   Lemma length_as_fold :
-   forall (C:Set) (l:list C),
+   forall (C:Type) (l:list C),
      length l = fold_right (fun (_:C) (n:nat) => S n) 0 l.
   Proof.
     simple induction l. reflexivity.
@@ -182,25 +182,25 @@ Section MapCard.
     rewrite H0. rewrite H1. reflexivity.
     intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. simpl in H0. left.
     rewrite H0. rewrite H1. reflexivity.
-    intros. simpl in H2. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1.
-    elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H1.
+    intros. simpl in H0. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H.
+    elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H.
     elim
-     (H0 (MapPut A m1 (Ndiv2 a) y) (Ndiv2 a) y (
+     (X0 (MapPut A m1 (Ndiv2 a) y) (Ndiv2 a) y (
         MapCard A m1) (MapCard A (MapPut A m1 (Ndiv2 a) y)) (
         refl_equal _) (refl_equal _) (refl_equal _)).
-    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. left.
+    intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. rewrite <- H0 in H1. left.
     assumption.
-    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3.
-    rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H3.
-    simpl in H3. rewrite <- H2 in H3. right. assumption.
-    intro H4. rewrite H4 in H1.
+    intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1.
+    rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H1.
+    simpl in H1. rewrite <- H0 in H1. right. assumption.
+    intro H4. rewrite H4 in H.
     elim
-     (H (MapPut A m0 (Ndiv2 a) y) (Ndiv2 a) y (
+     (X (MapPut A m0 (Ndiv2 a) y) (Ndiv2 a) y (
         MapCard A m0) (MapCard A (MapPut A m0 (Ndiv2 a) y)) (
         refl_equal _) (refl_equal _) (refl_equal _)).
-    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3.
+    intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. rewrite <- H0 in H1.
     left. assumption.
-    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. simpl in H3. rewrite <- H2 in H3.
+    intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. simpl in H1. rewrite <- H0 in H1.
     right. assumption.
   Qed.
 
@@ -239,15 +239,15 @@ Section MapCard.
     intros p H1. rewrite H1 in H. rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H.
     discriminate H.
     intro H0. rewrite H0 in H. rewrite (Nxor_eq _ _ H0). split with y. apply M1_semantics_1.
-    intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. elim (sumbool_of_bool (Nbit0 a)).
-    intro H2. rewrite H2 in H1. simpl in H1. elim (H0 (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)).
+    intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H. elim (sumbool_of_bool (Nbit0 a)).
+    intro H2. rewrite H2 in H. simpl in H. elim (X0 (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H)).
     intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_1 A a H2 m0 m1).
-    intro H2. rewrite H2 in H1. simpl in H1.
+    intro H2. rewrite H2 in H. simpl in H.
     rewrite
      (plus_comm (MapCard A (MapPut A m0 (Ndiv2 a) y)) (MapCard A m1))
-      in H1.
-    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1.
-    elim (H (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0.
+      in H.
+    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H.
+    elim (X (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H)). intros y0 H3. split with y0.
     rewrite <- H3. exact (MapGet_M2_bit_0_0 A a H2 m0 m1).
   Qed.
 
@@ -372,27 +372,27 @@ Section MapCard.
     simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H2. rewrite H2 in H.
     rewrite H in H1. simpl in H1. right. rewrite H1. assumption.
     intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. left. rewrite H1. assumption.
-    intros. simpl in H1. simpl in H2. elim (sumbool_of_bool (Nbit0 a)). intro H4.
-    rewrite H4 in H1. rewrite H1 in H3.
-    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H3.
+    intros. simpl in H1. simpl in H. elim (sumbool_of_bool (Nbit0 a)). intro H4.
+    rewrite H4 in H. rewrite H in H1.
+    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1.
     elim
-     (H0 (MapRemove A m1 (Ndiv2 a)) (Ndiv2 a) (
+     (X0 (MapRemove A m1 (Ndiv2 a)) (Ndiv2 a) (
         MapCard A m1) (MapCard A (MapRemove A m1 (Ndiv2 a)))
         (refl_equal _) (refl_equal _) (refl_equal _)).
-    intro H5. rewrite H5 in H2. left. rewrite H3. exact H2.
-    intro H5. rewrite H5 in H2.
+    simpl in H0;  intro H5. rewrite H5 in H0. left. rewrite H1. exact H0.
+    simpl in H0; intro H5. rewrite H5 in H0.
     rewrite <-
      (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a))))
-      in H2.
-    right. rewrite H3. exact H2.
-    intro H4. rewrite H4 in H1. rewrite H1 in H3.
-    rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H3.
+      in H0.
+    right. rewrite H1. exact H0.
+    intro H4. rewrite H4 in H. rewrite H in H1.
+    rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1.
     elim
-     (H (MapRemove A m0 (Ndiv2 a)) (Ndiv2 a) (
+     (X (MapRemove A m0 (Ndiv2 a)) (Ndiv2 a) (
         MapCard A m0) (MapCard A (MapRemove A m0 (Ndiv2 a)))
         (refl_equal _) (refl_equal _) (refl_equal _)).
-    intro H5. rewrite H5 in H2. left. rewrite H3. exact H2.
-    intro H5. rewrite H5 in H2. right. rewrite H3. exact H2.
+    simpl in H0; intro H5. rewrite H5 in H0. left. rewrite H1. exact H0.
+    simpl in H0; intro H5. rewrite H5 in H0. right. rewrite H1. exact H0.
   Qed.
 
   Lemma MapCard_Remove_ub :
@@ -448,25 +448,25 @@ Section MapCard.
     intros a y a0 H. simpl in H. elim (sumbool_of_bool (Neqb a a0)). intro H0.
     rewrite (Neqb_complete _ _ H0). split with y. exact (M1_semantics_1 A a0 y).
     intro H0. rewrite H0 in H. discriminate H.
-    intros. simpl in H1. elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2 in H1.
-    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1.
-    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0.
+    intros. simpl in H. elim (sumbool_of_bool (Nbit0 a)). intro H0. rewrite H0 in H.
+    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H.
+    rewrite (MapGet_M2_bit_0_1 A a H0 m0 m1). apply X0.
     change
       (S (MapCard A m0) + MapCard A (MapRemove A m1 (Ndiv2 a)) =
-       MapCard A m0 + MapCard A m1) in H1.
+       MapCard A m0 + MapCard A m1) in H.
     rewrite
      (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a))))
-      in H1.
-    exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
-    intro H2. rewrite H2 in H1. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H.
-    rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1.
+      in H.
+    exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H).
+    intro H2. rewrite H2 in H. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply X.
+    rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H.
     change
       (S (MapCard A (MapRemove A m0 (Ndiv2 a))) + MapCard A m1 =
-       MapCard A m0 + MapCard A m1) in H1.
+       MapCard A m0 + MapCard A m1) in H.
     rewrite
      (plus_comm (S (MapCard A (MapRemove A m0 (Ndiv2 a)))) (MapCard A m1))
-      in H1.
-    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
+      in H.
+    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H).
   Qed.
 
   Lemma MapCard_Remove_1_conv :
@@ -652,7 +652,7 @@ End MapCard.
 
 Section MapCard2.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapSubset_card_eq_1 :
    forall (n:nat) (m:Map A) (m':Map B),
@@ -708,7 +708,7 @@ End MapCard2.
 
 Section MapCard3.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapMerge_Card_lb_l :
    forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m.
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
index 99db86c6f0..6bc0cd914a 100644
--- a/theories/IntMap/Mapfold.v
+++ b/theories/IntMap/Mapfold.v
@@ -22,9 +22,9 @@ Require Import List.
 
 Section MapFoldResults.
 
-  Variable A : Set.
+  Variable A : Type.
 
-  Variable M : Set.
+  Variable M : Type.
   Variable neutral : M.
   Variable op : M -> M -> M.
 
@@ -268,17 +268,17 @@ End MapFoldResults.
 
 Section MapFoldDistr.
 
-  Variable A : Set.
+  Variable A : Type.
 
-  Variable M : Set.
+  Variable M : Type.
   Variable neutral : M.
   Variable op : M -> M -> M.
 
-  Variable M' : Set.
+  Variable M' : Type.
   Variable neutral' : M'.
   Variable op' : M' -> M' -> M'.
 
-  Variable N : Set.
+  Variable N : Type.
 
   Variable times : M -> N -> M'.
 
@@ -309,17 +309,17 @@ End MapFoldDistr.
 
 Section MapFoldDistrL.
 
-  Variable A : Set.
+  Variable A : Type.
 
-  Variable M : Set.
+  Variable M : Type.
   Variable neutral : M.
   Variable op : M -> M -> M.
 
-  Variable M' : Set.
+  Variable M' : Type.
   Variable neutral' : M'.
   Variable op' : M' -> M' -> M'.
 
-  Variable N : Set.
+  Variable N : Type.
 
   Variable times : N -> M -> M'.
 
@@ -341,7 +341,7 @@ End MapFoldDistrL.
 
 Section MapFoldExists.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Lemma MapFold_orb_1 :
    forall (f:ad -> A -> bool) (m:Map A) (pf:ad -> ad),
@@ -373,7 +373,7 @@ End MapFoldExists.
 
 Section DMergeDef.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Definition DMerge :=
     MapFold (Map A) (Map A) (M0 A) (MapMerge A) (fun (_:ad) (m:Map A) => m).
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v
index e551e47d9a..79e59a90e4 100644
--- a/theories/IntMap/Mapiter.v
+++ b/theories/IntMap/Mapiter.v
@@ -19,7 +19,7 @@ Require Import List.
 
 Section MapIter.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Section MapSweepDef.
 
@@ -180,16 +180,16 @@ Section MapIter.
     intro H1. rewrite (M1_semantics_2 _ a a1 a0 H1) in H. discriminate H.
 
     intros. elim (sumbool_of_bool (Nbit0 a)). intro H3.
-    rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H1.
-    rewrite <- (Ndiv2_double_plus_one a H3) in H2.
-    elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4.
+    rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H.
+    rewrite <- (Ndiv2_double_plus_one a H3) in H0.
+    elim (X0 (fun a0:ad => pf (Ndouble_plus_one a0)) (Ndiv2 a) y H H0). intros a'' H4. elim H4.
     intros y'' H5. simpl in |- *. elim (option_sum _ (MapSweep1 (fun a:ad => pf (Ndouble a)) m0)).
     intro H6. elim H6. intro r. elim r. intros a''' y''' H7. rewrite H7. split with a'''.
     split with y'''. reflexivity.
     intro H6. rewrite H6. split with a''. split with y''. assumption.
-    intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H1.
-    rewrite <- (Ndiv2_double a H3) in H2.
-    elim (H (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4.
+    intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H.
+    rewrite <- (Ndiv2_double a H3) in H0.
+    elim (X (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a) y H H0). intros a'' H4. elim H4.
     intros y'' H5. split with a''. split with y''. simpl in |- *. rewrite H5. reflexivity.
   Qed.
 
@@ -203,7 +203,7 @@ Section MapIter.
 
   End MapSweepDef.
 
-  Variable B : Set.
+  Variable B : Type.
 
   Fixpoint MapCollect1 (f:ad -> A -> Map B) (pf:ad -> ad) 
    (m:Map A) {struct m} : Map B :=
@@ -220,7 +220,7 @@ Section MapIter.
 
   Section MapFoldDef.
 
-    Variable M : Set.
+    Variable M : Type.
     Variable neutral : M.
     Variable op : M -> M -> M.
 
@@ -248,7 +248,7 @@ Section MapIter.
       trivial.
     Qed.
 
-    Variable State : Set.
+    Variable State : Type.
     Variable f : State -> ad -> A -> State * M.
 
     Fixpoint MapFold1_state (state:State) (pf:ad -> ad) 
@@ -271,7 +271,7 @@ Section MapIter.
     Definition MapFold_state (state:State) :=
       MapFold1_state state (fun a:ad => a).
 
-    Lemma pair_sp : forall (B C:Set) (x:B * C), x = (fst x, snd x).
+    Lemma pair_sp : forall (B C:Type) (x:B * C), x = (fst x, snd x).
     Proof.
       simple induction x. trivial.
     Qed.
@@ -364,23 +364,23 @@ Section MapIter.
             (fun a0:ad => pf (Ndouble a0)) m0)
          (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil)
             (fun a0:ad => pf (Ndouble_plus_one a0)) m1)) a = 
-    Some y) in H1.
+    Some y) in H.
     rewrite
      (alist_semantics_app
         (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil)
            (fun a0:ad => pf (Ndouble a0)) m0)
         (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil)
            (fun a0:ad => pf (Ndouble_plus_one a0)) m1) a)
-      in H1.
+      in H.
     elim
      (option_sum A
         (alist_semantics
            (MapFold1 alist anil aapp
               (fun (a0:ad) (y0:A) => acons (a0, y0) anil)
               (fun a0:ad => pf (Ndouble a0)) m0) a)).
-    intro H2. elim H2. intros y0 H3. elim (H (fun a0:ad => pf (Ndouble a0)) a y0 H3). intros a0 H4.
+    intro H2. elim H2. intros y0 H3. elim (X (fun a0:ad => pf (Ndouble a0)) a y0 H3). intros a0 H4.
     split with (Ndouble a0). assumption.
-    intro H2. rewrite H2 in H1. elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H1).
+    intro H2. rewrite H2 in H. elim (X0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H).
     intros a0 H3. split with (Ndouble_plus_one a0). assumption.
   Qed.
 
@@ -516,7 +516,7 @@ Section MapIter.
   Qed.
 
   Lemma fold_right_aapp :
-   forall (M:Set) (neutral:M) (op:M -> M -> M),
+   forall (M:Type) (neutral:M) (op:M -> M -> M),
      (forall a b c:M, op (op a b) c = op a (op b c)) ->
      (forall a:M, op neutral a = a) ->
      forall (f:ad -> A -> M) (l l':alist),
@@ -535,7 +535,7 @@ Section MapIter.
   Qed.
 
   Lemma MapFold_as_fold_1 :
-   forall (M:Set) (neutral:M) (op:M -> M -> M),
+   forall (M:Type) (neutral:M) (op:M -> M -> M),
      (forall a b c:M, op (op a b) c = op a (op b c)) ->
      (forall a:M, op neutral a = a) ->
      (forall a:M, op a neutral = a) ->
@@ -554,7 +554,7 @@ Section MapIter.
   Qed.
 
   Lemma MapFold_as_fold :
-   forall (M:Set) (neutral:M) (op:M -> M -> M),
+   forall (M:Type) (neutral:M) (op:M -> M -> M),
      (forall a b c:M, op (op a b) c = op a (op b c)) ->
      (forall a:M, op neutral a = a) ->
      (forall a:M, op a neutral = a) ->
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v
index f4b5bbe92e..56396cdade 100644
--- a/theories/IntMap/Maplists.v
+++ b/theories/IntMap/Maplists.v
@@ -340,7 +340,7 @@ Section MapLists.
 
   Section ListOfDomDef.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Definition ad_list_of_dom :=
     MapFold A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil).
@@ -418,7 +418,7 @@ Section MapLists.
   End ListOfDomDef.
 
   Lemma ad_list_of_dom_Dom_1 :
-   forall (A:Set) (m:Map A) (pf:ad -> ad),
+   forall (A:Type) (m:Map A) (pf:ad -> ad),
      MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) pf
        m =
      MapFold1 unit (list ad) nil (app (A:=ad))
@@ -429,7 +429,7 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_of_dom_Dom :
-   forall (A:Set) (m:Map A),
+   forall (A:Type) (m:Map A),
      ad_list_of_dom A m = ad_list_of_dom unit (MapDom A m).
   Proof.
     intros. exact (ad_list_of_dom_Dom_1 A m (fun a0:ad => a0)).
diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index 1db99b3688..74b7163128 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -20,7 +20,7 @@ Require Import Mapiter.
 
 Section MapSubsetDef.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Definition MapSubset (m:Map A) (m':Map B) :=
     forall a:ad, in_dom A a m = true -> in_dom B a m' = true.
@@ -105,7 +105,7 @@ End MapSubsetDef.
 
 Section MapSubsetOrder.
 
-  Variables A B C : Set.
+  Variables A B C : Type.
 
   Lemma MapSubset_refl : forall m:Map A, MapSubset A A m m.
   Proof.
@@ -165,7 +165,7 @@ End FSubsetOrder.
 
 Section MapSubsetExtra.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapSubset_Dom_1 :
    forall (m:Map A) (m':Map B),
@@ -303,7 +303,7 @@ Section MapSubsetExtra.
     exact (MapSubset_imp_2 _ _ _ _ H1).
   Qed.
 
-  Variables C D : Set.
+  Variables C D : Type.
 
   Lemma MapSubset_DomRestrTo_mono :
    forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
@@ -338,7 +338,7 @@ End MapSubsetExtra.
 
 Section MapDisjointDef.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Definition MapDisjoint (m:Map A) (m':Map B) :=
     forall a:ad, in_dom A a m = true -> in_dom B a m' = true -> False.
@@ -414,7 +414,7 @@ End MapDisjointDef.
 
 Section MapDisjointExtra.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Lemma MapDisjoint_ext :
    forall (m0 m1:Map A) (m2 m3:Map B),
@@ -549,7 +549,7 @@ Section MapDisjointExtra.
     apply MapDomRestrBy_m_empty.
   Qed.
 
-  Variable C : Set.
+  Variable C : Type.
 
   Lemma MapDomRestr_disjoint :
    forall (m:Map A) (m':Map B) (m'':Map C),
@@ -576,7 +576,7 @@ Section MapDisjointExtra.
     intros. elim (andb_prop _ _ H0). intros. rewrite H1 in H. rewrite H2 in H. discriminate H.
   Qed.
 
-  Variable D : Set.
+  Variable D : Type.
 
   Lemma MapSubset_Disjoint :
    forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),