From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 5 Jun 2009 13:39:59 +0000
Subject: Adapted to work with Coq 8.2-1

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v    | 120 +++++++++++++-------------
 lib/Floats.v    |   2 +-
 lib/Inclusion.v |  24 +++---
 lib/Integers.v  |   6 +-
 lib/Iteration.v |   8 +-
 lib/Lattice.v   |  27 ++----
 lib/Maps.v      | 260 ++++++++++++++++++++++++++++----------------------------
 lib/Ordered.v   |  19 +++++
 lib/Parmov.v    |   8 +-
 9 files changed, 239 insertions(+), 235 deletions(-)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index a79ea29c..9e2199c1 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -31,7 +31,7 @@ Require Import Wf_nat.
   that have identical contents are equal. *)
 
 Axiom extensionality:
-  forall (A B: Set) (f g : A -> B),
+  forall (A B: Type) (f g : A -> B),
   (forall x, f x = g x) -> f = g.
 
 Axiom proof_irrelevance:
@@ -114,7 +114,7 @@ Proof.
 Qed.
 
 Lemma peq_true:
-  forall (A: Set) (x: positive) (a b: A), (if peq x x then a else b) = a.
+  forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a.
 Proof.
   intros. case (peq x x); intros.
   auto.
@@ -122,7 +122,7 @@ Proof.
 Qed.
 
 Lemma peq_false:
-  forall (A: Set) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
+  forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
 Proof.
   intros. case (peq x y); intros.
   elim H; auto.
@@ -223,7 +223,7 @@ Proof.
   intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
 Qed.
 
-Variable A: Set.
+Variable A: Type.
 Variable v1: A.
 Variable f: positive -> A -> A.
 
@@ -289,7 +289,7 @@ End POSITIVE_ITERATION.
 Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec.
 
 Lemma zeq_true:
-  forall (A: Set) (x: Z) (a b: A), (if zeq x x then a else b) = a.
+  forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a.
 Proof.
   intros. case (zeq x x); intros.
   auto.
@@ -297,7 +297,7 @@ Proof.
 Qed.
 
 Lemma zeq_false:
-  forall (A: Set) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
+  forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
 Proof.
   intros. case (zeq x y); intros.
   elim H; auto.
@@ -309,7 +309,7 @@ Open Scope Z_scope.
 Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.
 
 Lemma zlt_true:
-  forall (A: Set) (x y: Z) (a b: A), 
+  forall (A: Type) (x y: Z) (a b: A), 
   x < y -> (if zlt x y then a else b) = a.
 Proof.
   intros. case (zlt x y); intros.
@@ -318,7 +318,7 @@ Proof.
 Qed.
 
 Lemma zlt_false:
-  forall (A: Set) (x y: Z) (a b: A), 
+  forall (A: Type) (x y: Z) (a b: A), 
   x >= y -> (if zlt x y then a else b) = b.
 Proof.
   intros. case (zlt x y); intros.
@@ -329,7 +329,7 @@ Qed.
 Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.
 
 Lemma zle_true:
-  forall (A: Set) (x y: Z) (a b: A), 
+  forall (A: Type) (x y: Z) (a b: A), 
   x <= y -> (if zle x y then a else b) = a.
 Proof.
   intros. case (zle x y); intros.
@@ -338,7 +338,7 @@ Proof.
 Qed.
 
 Lemma zle_false:
-  forall (A: Set) (x y: Z) (a b: A), 
+  forall (A: Type) (x y: Z) (a b: A), 
   x > y -> (if zle x y then a else b) = b.
 Proof.
   intros. case (zle x y); intros.
@@ -573,7 +573,7 @@ Set Implicit Arguments.
 
 (** Mapping a function over an option type. *)
 
-Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B :=
+Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B :=
   match x with
   | None => None
   | Some y => Some (f y)
@@ -581,7 +581,7 @@ Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B :=
 
 (** Mapping a function over a sum type. *)
 
-Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C :=
+Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C :=
   match x with
   | inl y => inl C (f y)
   | inr z => inr B z
@@ -592,7 +592,7 @@ Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C :=
 Hint Resolve in_eq in_cons: coqlib.
 
 Lemma nth_error_in:
-  forall (A: Set) (n: nat) (l: list A) (x: A),
+  forall (A: Type) (n: nat) (l: list A) (x: A),
   List.nth_error l n = Some x -> In x l.
 Proof.
   induction n; simpl.
@@ -606,7 +606,7 @@ Qed.
 Hint Resolve nth_error_in: coqlib.
 
 Lemma nth_error_nil:
-  forall (A: Set) (idx: nat), nth_error (@nil A) idx = None.
+  forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
 Proof.
   induction idx; simpl; intros; reflexivity.
 Qed.
@@ -615,7 +615,7 @@ Hint Resolve nth_error_nil: coqlib.
 (** Properties of [List.incl] (list inclusion). *)
 
 Lemma incl_cons_inv:
-  forall (A: Set) (a: A) (b c: list A),
+  forall (A: Type) (a: A) (b c: list A),
   incl (a :: b) c -> incl b c.
 Proof.
   unfold incl; intros. apply H. apply in_cons. auto.
@@ -623,14 +623,14 @@ Qed.
 Hint Resolve incl_cons_inv: coqlib.
 
 Lemma incl_app_inv_l:
-  forall (A: Set) (l1 l2 m: list A),
+  forall (A: Type) (l1 l2 m: list A),
   incl (l1 ++ l2) m -> incl l1 m.
 Proof.
   unfold incl; intros. apply H. apply in_or_app. left; assumption.
 Qed.
 
 Lemma incl_app_inv_r:
-  forall (A: Set) (l1 l2 m: list A),
+  forall (A: Type) (l1 l2 m: list A),
   incl (l1 ++ l2) m -> incl l2 m.
 Proof.
   unfold incl; intros. apply H. apply in_or_app. right; assumption.
@@ -639,7 +639,7 @@ Qed.
 Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
 
 Lemma incl_same_head:
-  forall (A: Set) (x: A) (l1 l2: list A),
+  forall (A: Type) (x: A) (l1 l2: list A),
   incl l1 l2 -> incl (x::l1) (x::l2).
 Proof.
   intros; red; simpl; intros. intuition. 
@@ -648,7 +648,7 @@ Qed.
 (** Properties of [List.map] (mapping a function over a list). *)
 
 Lemma list_map_exten:
-  forall (A B: Set) (f f': A -> B) (l: list A),
+  forall (A B: Type) (f f': A -> B) (l: list A),
   (forall x, In x l -> f x = f' x) ->
   List.map f' l = List.map f l.
 Proof.
@@ -660,21 +660,21 @@ Proof.
 Qed.
 
 Lemma list_map_compose:
-  forall (A B C: Set) (f: A -> B) (g: B -> C) (l: list A),
+  forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A),
   List.map g (List.map f l) = List.map (fun x => g(f x)) l.
 Proof.
   induction l; simpl. reflexivity. rewrite IHl; reflexivity.
 Qed.
 
 Lemma list_map_identity:
-  forall (A: Set) (l: list A),
+  forall (A: Type) (l: list A),
   List.map (fun (x:A) => x) l = l.
 Proof.
   induction l; simpl; congruence.
 Qed.
 
 Lemma list_map_nth:
-  forall (A B: Set) (f: A -> B) (l: list A) (n: nat),
+  forall (A B: Type) (f: A -> B) (l: list A) (n: nat),
   nth_error (List.map f l) n = option_map f (nth_error l n).
 Proof.
   induction l; simpl; intros.
@@ -683,14 +683,14 @@ Proof.
 Qed.
 
 Lemma list_length_map:
-  forall (A B: Set) (f: A -> B) (l: list A),
+  forall (A B: Type) (f: A -> B) (l: list A),
   List.length (List.map f l) = List.length l.
 Proof.
   induction l; simpl; congruence.
 Qed.
 
 Lemma list_in_map_inv:
-  forall (A B: Set) (f: A -> B) (l: list A) (y: B),
+  forall (A B: Type) (f: A -> B) (l: list A) (y: B),
   In y (List.map f l) -> exists x:A, y = f x /\ In x l.
 Proof.
   induction l; simpl; intros.
@@ -702,7 +702,7 @@ Proof.
 Qed.
 
 Lemma list_append_map:
-  forall (A B: Set) (f: A -> B) (l1 l2: list A),
+  forall (A B: Type) (f: A -> B) (l1 l2: list A),
   List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
 Proof.
   induction l1; simpl; intros.
@@ -712,19 +712,19 @@ Qed.
 (** Properties of list membership. *)
 
 Lemma in_cns:
-  forall (A: Set) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
+  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
 Proof.
   intros. simpl. tauto.
 Qed.
 
 Lemma in_app:
-  forall (A: Set) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
+  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
 Proof.
   intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
 Qed.
 
 Lemma list_in_insert:
-  forall (A: Set) (x: A) (l1 l2: list A) (y: A),
+  forall (A: Type) (x: A) (l1 l2: list A) (y: A),
   In x (l1 ++ l2) -> In x (l1 ++ y :: l2).
 Proof.
   intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
@@ -733,25 +733,25 @@ Qed.
 (** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements 
   in common. *)
 
-Definition list_disjoint (A: Set) (l1 l2: list A) : Prop :=
+Definition list_disjoint (A: Type) (l1 l2: list A) : Prop :=
   forall (x y: A), In x l1 -> In y l2 -> x <> y.
 
 Lemma list_disjoint_cons_left:
-  forall (A: Set) (a: A) (l1 l2: list A),
+  forall (A: Type) (a: A) (l1 l2: list A),
   list_disjoint (a :: l1) l2 -> list_disjoint l1 l2.
 Proof.
   unfold list_disjoint; simpl; intros. apply H; tauto. 
 Qed.
 
 Lemma list_disjoint_cons_right:
-  forall (A: Set) (a: A) (l1 l2: list A),
+  forall (A: Type) (a: A) (l1 l2: list A),
   list_disjoint l1 (a :: l2) -> list_disjoint l1 l2.
 Proof.
   unfold list_disjoint; simpl; intros. apply H; tauto. 
 Qed.
 
 Lemma list_disjoint_notin:
-  forall (A: Set) (l1 l2: list A) (a: A),
+  forall (A: Type) (l1 l2: list A) (a: A),
   list_disjoint l1 l2 -> In a l1 -> ~(In a l2).
 Proof.
   unfold list_disjoint; intros; red; intros. 
@@ -759,7 +759,7 @@ Proof.
 Qed.
 
 Lemma list_disjoint_sym:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   list_disjoint l1 l2 -> list_disjoint l2 l1.
 Proof.
   unfold list_disjoint; intros. 
@@ -767,7 +767,7 @@ Proof.
 Qed.
 
 Lemma list_disjoint_dec:
-  forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
+  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
   {list_disjoint l1 l2} + {~list_disjoint l1 l2}.
 Proof.
   induction l1; intros.
@@ -784,7 +784,7 @@ Defined.
 (** [list_norepet l] holds iff the list [l] contains no repetitions,
   i.e. no element occurs twice. *)
 
-Inductive list_norepet (A: Set) : list A -> Prop :=
+Inductive list_norepet (A: Type) : list A -> Prop :=
   | list_norepet_nil:
       list_norepet nil
   | list_norepet_cons:
@@ -792,7 +792,7 @@ Inductive list_norepet (A: Set) : list A -> Prop :=
       ~(In hd tl) -> list_norepet tl -> list_norepet (hd :: tl).
 
 Lemma list_norepet_dec:
-  forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
+  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
   {list_norepet l} + {~list_norepet l}.
 Proof.
   induction l.
@@ -805,7 +805,7 @@ Proof.
 Defined.
 
 Lemma list_map_norepet:
-  forall (A B: Set) (f: A -> B) (l: list A),
+  forall (A B: Type) (f: A -> B) (l: list A),
   list_norepet l ->
   (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
   list_norepet (List.map f l).
@@ -821,7 +821,7 @@ Proof.
 Qed.
 
 Remark list_norepet_append_commut:
-  forall (A: Set) (a b: list A),
+  forall (A: Type) (a b: list A),
   list_norepet (a ++ b) -> list_norepet (b ++ a).
 Proof.
   intro A.
@@ -844,7 +844,7 @@ Proof.
 Qed.
 
 Lemma list_norepet_app:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   list_norepet (l1 ++ l2) <->
   list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2.
 Proof.
@@ -860,7 +860,7 @@ Proof.
 Qed.
 
 Lemma list_norepet_append:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
   list_norepet (l1 ++ l2).
 Proof.
@@ -868,14 +868,14 @@ Proof.
 Qed.
 
 Lemma list_norepet_append_right:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   list_norepet (l1 ++ l2) -> list_norepet l2.
 Proof.
   generalize list_norepet_app; firstorder.
 Qed.
 
 Lemma list_norepet_append_left:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   list_norepet (l1 ++ l2) -> list_norepet l1.
 Proof.
   generalize list_norepet_app; firstorder.
@@ -883,14 +883,14 @@ Qed.
 
 (** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
 
-Inductive is_tail (A: Set): list A -> list A -> Prop :=
+Inductive is_tail (A: Type): list A -> list A -> Prop :=
   | is_tail_refl:
       forall c, is_tail c c
   | is_tail_cons:
       forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
 
 Lemma is_tail_in:
-  forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
+  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
 Proof.
   induction c2; simpl; intros.
   inversion H.
@@ -898,7 +898,7 @@ Proof.
 Qed.
 
 Lemma is_tail_cons_left:
-  forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
+  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
 Proof.
   induction c2; intros; inversion H.
   constructor. constructor. constructor. auto. 
@@ -907,13 +907,13 @@ Qed.
 Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
 
 Lemma is_tail_incl:
-  forall (A: Set) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
+  forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
 Proof.
   induction 1; eauto with coqlib.
 Qed.
 
 Lemma is_tail_trans:
-  forall (A: Set) (l1 l2: list A),
+  forall (A: Type) (l1 l2: list A),
   is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.
 Proof.
   induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
@@ -924,8 +924,8 @@ Qed.
 
 Section FORALL2.
 
-Variable A: Set.
-Variable B: Set.
+Variable A: Type.
+Variable B: Type.
 Variable P: A -> B -> Prop.
 
 Inductive list_forall2: list A -> list B -> Prop :=
@@ -940,7 +940,7 @@ Inductive list_forall2: list A -> list B -> Prop :=
 End FORALL2.
 
 Lemma list_forall2_imply:
-  forall (A B: Set) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
+  forall (A B: Type) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
   list_forall2 P1 l1 l2 ->
   forall (P2: A -> B -> Prop),
   (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
@@ -954,45 +954,45 @@ Qed.
 
 (** Dropping the first or first two elements of a list. *)
 
-Definition list_drop1 (A: Set) (x: list A) :=
+Definition list_drop1 (A: Type) (x: list A) :=
   match x with nil => nil | hd :: tl => tl end.
-Definition list_drop2 (A: Set) (x: list A) :=
+Definition list_drop2 (A: Type) (x: list A) :=
   match x with nil => nil | hd :: nil => nil | hd1 :: hd2 :: tl => tl end.
 
 Lemma list_drop1_incl:
-  forall (A: Set) (x: A) (l: list A), In x (list_drop1 l) -> In x l.
+  forall (A: Type) (x: A) (l: list A), In x (list_drop1 l) -> In x l.
 Proof.
   intros. destruct l. elim H. simpl in H. auto with coqlib.
 Qed.
 
 Lemma list_drop2_incl:
-  forall (A: Set) (x: A) (l: list A), In x (list_drop2 l) -> In x l.
+  forall (A: Type) (x: A) (l: list A), In x (list_drop2 l) -> In x l.
 Proof.
   intros. destruct l. elim H. destruct l. elim H.
   simpl in H. auto with coqlib.
 Qed.
 
 Lemma list_drop1_norepet:
-  forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop1 l).
+  forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop1 l).
 Proof.
   intros. destruct l; simpl. constructor. inversion H. auto.
 Qed.
 
 Lemma list_drop2_norepet:
-  forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop2 l).
+  forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop2 l).
 Proof.
   intros. destruct l; simpl. constructor.
   destruct l; simpl. constructor. inversion H. inversion H3. auto.
 Qed.
 
 Lemma list_map_drop1:
-  forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
+  forall (A B: Type) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
 Proof.
   intros; destruct l; reflexivity.
 Qed.
 
 Lemma list_map_drop2:
-  forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
+  forall (A B: Type) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
 Proof.
   intros; destruct l. reflexivity. destruct l; reflexivity.
 Qed.
@@ -1014,9 +1014,9 @@ Qed.
 
 Section DECIDABLE_EQUALITY.
 
-Variable A: Set.
+Variable A: Type.
 Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
-Variable B: Set.
+Variable B: Type.
 
 Lemma dec_eq_true:
   forall (x: A) (ifso ifnot: B),
diff --git a/lib/Floats.v b/lib/Floats.v
index 6857236d..2e60d73e 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -23,7 +23,7 @@
 Require Import Coqlib.
 Require Import Integers.
 
-Parameter float: Set.
+Parameter float: Type.
 
 Module Float.
 
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
index 728a7252..77f5d849 100644
--- a/lib/Inclusion.v
+++ b/lib/Inclusion.v
@@ -51,7 +51,7 @@ Ltac all_app e :=
 (** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem
   are taken from the CoqArt book, chapt. 16. *)
 
-Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
+Inductive bin : Type := node : bin->bin->bin | leaf : nat->bin.
 
 Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
   match t with
@@ -91,7 +91,7 @@ Fixpoint sort_bin (t:bin) : bin :=
   end.
 
 Section assoc_eq.
- Variables (A : Set)(f : A->A->A).
+ Variables (A : Type)(f : A->A->A).
  Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z.
 
  Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
@@ -147,7 +147,7 @@ Ltac model_aux_app l v :=
   end.
 
 Theorem In_permute_app_head :
-  forall A:Set, forall r:A, forall x y l:list A,
+  forall A:Type, forall r:A, forall x y l:list A,
    In r (x++y++l) -> In r (y++x++l).
 intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)).
 repeat rewrite ass_app; auto with datatypes.
@@ -155,7 +155,7 @@ Qed.
 
 Theorem insert_bin_included : 
   forall x:nat, forall t2:bin,
-  forall (A:Set) (r:A) (l:list (list A))(def:list A), 
+  forall (A:Type) (r:A) (l:list (list A))(def:list A), 
      In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) ->
      In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)).
 intros x t2; induction t2.
@@ -181,7 +181,7 @@ apply In_permute_app_head; assumption.
 Qed.
 
 Theorem in_or_insert_bin :
-  forall (n:nat) (t2:bin) (A:Set)(r:A)(l:list (list A)) (def:list A),
+  forall (n:nat) (t2:bin) (A:Type)(r:A)(l:list (list A)) (def:list A),
   In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) ->
   In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)).
 intros n t2 A r l def; induction t2.
@@ -198,7 +198,7 @@ simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto.
 Qed.
 
 Theorem sort_included :
-  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
     In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) ->
     In r (bin_A (list A) (app (A:=A)) l def t).
 induction t.
@@ -213,7 +213,7 @@ simpl;intros;assumption.
 Qed.
 
 Theorem sort_included2 :
-  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
     In r (bin_A (list A) (app (A:=A)) l def t) ->
     In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)).
 induction t.
@@ -226,7 +226,7 @@ simpl; auto.
 Qed.
 
 Theorem in_remove_head :
-  forall (A:Set)(x:A)(l1 l2 l3:list A),
+  forall (A:Type)(x:A)(l1 l2 l3:list A),
   In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3).
 intros A x l1 l2 l3 H H1.
 elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
@@ -257,7 +257,7 @@ Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool :=
 Theorem check_all_leaves_sound :
   forall x t2,
     check_all_leaves x t2 = true ->
-    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    forall (A:Type)(r:A)(l:list(list A))(def:list A),
     In r (bin_A (list A) (app (A:=A)) l def t2) ->
     In r (nth x l def).
 intros x t2; induction t2; simpl.
@@ -270,7 +270,7 @@ Qed.
 
 Theorem remove_all_leaves_sound :
   forall x t2,
-  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  forall (A:Type)(r:A)(l:list(list A))(def:list A),
   In r (bin_A (list A) (app(A:=A)) l def t2) ->
   In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/
   In r (nth x l def).
@@ -293,7 +293,7 @@ Qed.
 Theorem test_inclusion_sound :
   forall t1 t2:bin,
   test_inclusion t1 t2 = true ->
-  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  forall (A:Type)(r:A)(l:list(list A))(def:list A),
   In r (bin_A (list A)(app(A:=A)) l def t2) ->
   In r (bin_A (list A)(app(A:=A)) l def t1).
 intros t1; induction t1.
@@ -317,7 +317,7 @@ Qed.
 Theorem inclusion_theorem :
   forall t1 t2 : bin,
     test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true ->
-    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    forall (A:Type)(r:A)(l:list(list A))(def:list A),
     In r (bin_A (list A) (app(A:=A)) l def t2) ->
     In r (bin_A (list A) (app(A:=A)) l def t1).
 intros t1 t2 Heq A r l def H.
diff --git a/lib/Integers.v b/lib/Integers.v
index ceda8512..1eb59c5c 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -23,7 +23,7 @@ Definition half_modulus : Z := modulus / 2.
 
 (** * Comparisons *)
 
-Inductive comparison : Set :=
+Inductive comparison : Type :=
   | Ceq : comparison               (**r same *)
   | Cne : comparison               (**r different *)
   | Clt : comparison               (**r less than *)
@@ -57,7 +57,7 @@ Definition swap_comparison (c: comparison): comparison :=
   integer (type [Z]) plus a proof that it is in the range 0 (included) to
   [modulus] (excluded. *)
 
-Record int: Set := mkint { intval: Z; intrange: 0 <= intval < modulus }.
+Record int: Type := mkint { intval: Z; intrange: 0 <= intval < modulus }.
 
 Module Int.
 
@@ -289,7 +289,7 @@ Definition is_power2 (x: int) : option int :=
 >>
 *)
 
-Inductive rlw_state: Set :=
+Inductive rlw_state: Type :=
   | RLW_S0 : rlw_state
   | RLW_S1 : rlw_state
   | RLW_S2 : rlw_state
diff --git a/lib/Iteration.v b/lib/Iteration.v
index cabe5b82..24835da2 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -18,9 +18,9 @@ Require Import Max.
 
 Module Type ITER.
 Variable iterate
-     : forall A B : Set, (A -> B + A) -> A -> option B.
+     : forall A B : Type, (A -> B + A) -> A -> option B.
 Hypothesis iterate_prop
-     : forall (A B : Set) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
+     : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
        (forall a : A, P a ->
            match step a with inl b => Q b | inr a' => P a' end) ->
        forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b.
@@ -39,7 +39,7 @@ Module PrimIter: ITER.
 
 Section ITERATION.
 
-Variables A B: Set.
+Variables A B: Type.
 Variable step: A -> B + A.
 
 (** The [step] parameter represents one step of the iteration.  From a 
@@ -174,7 +174,7 @@ Module GenIter: ITER.
 
 Section ITERATION.
 
-Variables A B: Set.
+Variables A B: Type.
 Variable step: A -> B + A.
 
 Definition B_le (x y: option B) : Prop := x = None \/ y = x.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 3c390069..1d58ee5a 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -25,7 +25,7 @@ Require Import FSets.
 
 Module Type SEMILATTICE.
 
-  Variable t: Set.
+  Variable t: Type.
   Variable eq: t -> t -> Prop.
   Hypothesis eq_refl: forall x, eq x x.
   Hypothesis eq_sym: forall x y, eq x y -> eq y x.
@@ -49,24 +49,9 @@ End SEMILATTICE.
 
 Module Type SEMILATTICE_WITH_TOP.
 
-  Variable t: Set.
-  Variable eq: t -> t -> Prop.
-  Hypothesis eq_refl: forall x, eq x x.
-  Hypothesis eq_sym: forall x y, eq x y -> eq y x.
-  Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
-  Variable beq: t -> t -> bool.
-  Hypothesis beq_correct: forall x y, beq x y = true -> eq x y.
-  Variable ge: t -> t -> Prop.
-  Hypothesis ge_refl: forall x y, eq x y -> ge x y.
-  Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Variable bot: t.
-  Hypothesis ge_bot: forall x, ge x bot.
+  Include Type SEMILATTICE.
   Variable top: t.
   Hypothesis ge_top: forall x, ge top x.
-  Variable lub: t -> t -> t.
-  Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x).
-  Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
 
 End SEMILATTICE_WITH_TOP.
 
@@ -78,11 +63,11 @@ End SEMILATTICE_WITH_TOP.
 
 Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
 
-Inductive t_ : Set :=
+Inductive t_ : Type :=
   | Bot_except: PTree.t L.t -> t_
   | Top_except: PTree.t L.t -> t_.
 
-Definition t: Set := t_.
+Definition t: Type := t_.
 
 Definition get (p: positive) (x: t) : L.t :=
   match x with
@@ -333,12 +318,12 @@ End LFSet.
 
 Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.
 
-Inductive t_ : Set :=
+Inductive t_ : Type :=
   | Bot: t_
   | Inj: X.t -> t_
   | Top: t_.
 
-Definition t : Set := t_.
+Definition t : Type := t_.
 
 Definition eq (x y: t) := (x = y).
 Definition eq_refl: forall x, eq x x := (@refl_equal t).
diff --git a/lib/Maps.v b/lib/Maps.v
index 4209fe6e..a277e677 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -39,46 +39,46 @@ Set Implicit Arguments.
 (** * The abstract signatures of trees *)
 
 Module Type TREE.
-  Variable elt: Set.
+  Variable elt: Type.
   Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
-  Variable t: Set -> Set.
-  Variable eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+  Variable t: Type -> Type.
+  Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
                 forall (a b: t A), {a = b} + {a <> b}.
-  Variable empty: forall (A: Set), t A.
-  Variable get: forall (A: Set), elt -> t A -> option A.
-  Variable set: forall (A: Set), elt -> A -> t A -> t A.
-  Variable remove: forall (A: Set), elt -> t A -> t A.
+  Variable empty: forall (A: Type), t A.
+  Variable get: forall (A: Type), elt -> t A -> option A.
+  Variable set: forall (A: Type), elt -> A -> t A -> t A.
+  Variable remove: forall (A: Type), elt -> t A -> t A.
 
   (** The ``good variables'' properties for trees, expressing
     commutations between [get], [set] and [remove]. *)
   Hypothesis gempty:
-    forall (A: Set) (i: elt), get i (empty A) = None.
+    forall (A: Type) (i: elt), get i (empty A) = None.
   Hypothesis gss:
-    forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
+    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
   Hypothesis gso:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Hypothesis gsspec:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then Some x else get i m.
   Hypothesis gsident:
-    forall (A: Set) (i: elt) (m: t A) (v: A),
+    forall (A: Type) (i: elt) (m: t A) (v: A),
     get i m = Some v -> set i v m = m.
   (* We could implement the following, but it's not needed for the moment.
     Hypothesis grident:
-      forall (A: Set) (i: elt) (m: t A) (v: A),
+      forall (A: Type) (i: elt) (m: t A) (v: A),
       get i m = None -> remove i m = m.
   *)
   Hypothesis grs:
-    forall (A: Set) (i: elt) (m: t A), get i (remove i m) = None.
+    forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
   Hypothesis gro:
-    forall (A: Set) (i j: elt) (m: t A),
+    forall (A: Type) (i j: elt) (m: t A),
     i <> j -> get i (remove j m) = get i m.
 
   (** Extensional equality between trees. *)
-  Variable beq: forall (A: Set), (A -> A -> bool) -> t A -> t A -> bool.
+  Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
   Hypothesis beq_correct:
-    forall (A: Set) (P: A -> A -> Prop) (cmp: A -> A -> bool),
+    forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool),
     (forall (x y: A), cmp x y = true -> P x y) ->
     forall (t1 t2: t A), beq cmp t1 t2 = true ->
     forall (x: elt),
@@ -90,43 +90,43 @@ Module Type TREE.
 
   (** Applying a function to all data of a tree. *)
   Variable map:
-    forall (A B: Set), (elt -> A -> B) -> t A -> t B.
+    forall (A B: Type), (elt -> A -> B) -> t A -> t B.
   Hypothesis gmap:
-    forall (A B: Set) (f: elt -> A -> B) (i: elt) (m: t A),
+    forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
     get i (map f m) = option_map (f i) (get i m).
 
   (** Applying a function pairwise to all data of two trees. *)
   Variable combine:
-    forall (A: Set), (option A -> option A -> option A) -> t A -> t A -> t A.
+    forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.
   Hypothesis gcombine:
-    forall (A: Set) (f: option A -> option A -> option A)
+    forall (A: Type) (f: option A -> option A -> option A)
            (m1 m2: t A) (i: elt),
     f None None = None ->
     get i (combine f m1 m2) = f (get i m1) (get i m2).
   Hypothesis combine_commut:
-    forall (A: Set) (f g: option A -> option A -> option A),
+    forall (A: Type) (f g: option A -> option A -> option A),
     (forall (i j: option A), f i j = g j i) ->
     forall (m1 m2: t A),
     combine f m1 m2 = combine g m2 m1.
 
   (** Enumerating the bindings of a tree. *)
   Variable elements:
-    forall (A: Set), t A -> list (elt * A).
+    forall (A: Type), t A -> list (elt * A).
   Hypothesis elements_correct:
-    forall (A: Set) (m: t A) (i: elt) (v: A),
+    forall (A: Type) (m: t A) (i: elt) (v: A),
     get i m = Some v -> In (i, v) (elements m).
   Hypothesis elements_complete:
-    forall (A: Set) (m: t A) (i: elt) (v: A),
+    forall (A: Type) (m: t A) (i: elt) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Hypothesis elements_keys_norepet:
-    forall (A: Set) (m: t A), 
+    forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
 
   (** Folding a function over all bindings of a tree. *)
   Variable fold:
-    forall (A B: Set), (B -> elt -> A -> B) -> t A -> B -> B.
+    forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B.
   Hypothesis fold_spec:
-    forall (A B: Set) (f: B -> elt -> A -> B) (v: B) (m: t A),
+    forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
 End TREE.
@@ -134,27 +134,27 @@ End TREE.
 (** * The abstract signatures of maps *)
 
 Module Type MAP.
-  Variable elt: Set.
+  Variable elt: Type.
   Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
-  Variable t: Set -> Set.
-  Variable init: forall (A: Set), A -> t A.
-  Variable get: forall (A: Set), elt -> t A -> A.
-  Variable set: forall (A: Set), elt -> A -> t A -> t A.
+  Variable t: Type -> Type.
+  Variable init: forall (A: Type), A -> t A.
+  Variable get: forall (A: Type), elt -> t A -> A.
+  Variable set: forall (A: Type), elt -> A -> t A -> t A.
   Hypothesis gi:
-    forall (A: Set) (i: elt) (x: A), get i (init x) = x.
+    forall (A: Type) (i: elt) (x: A), get i (init x) = x.
   Hypothesis gss:
-    forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
+    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
   Hypothesis gso:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Hypothesis gsspec:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then x else get i m.
   Hypothesis gsident:
-    forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
-  Variable map: forall (A B: Set), (A -> B) -> t A -> t B.
+    forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+  Variable map: forall (A B: Type), (A -> B) -> t A -> t B.
   Hypothesis gmap:
-    forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
     get i (map f m) = f(get i m).
 End MAP.
 
@@ -164,7 +164,7 @@ Module PTree <: TREE.
   Definition elt := positive.
   Definition elt_eq := peq.
 
-  Inductive tree (A : Set) : Set :=
+  Inductive tree (A : Type) : Type :=
     | Leaf : tree A
     | Node : tree A -> option A -> tree A -> tree A
   .
@@ -173,7 +173,7 @@ Module PTree <: TREE.
 
   Definition t := tree.
 
-  Theorem eq : forall (A : Set),
+  Theorem eq : forall (A : Type),
     (forall (x y: A), {x=y} + {x<>y}) ->
     forall (a b : t A), {a = b} + {a <> b}.
   Proof.
@@ -182,9 +182,9 @@ Module PTree <: TREE.
     generalize o o0; decide equality.
   Qed.
 
-  Definition empty (A : Set) := (Leaf : t A).
+  Definition empty (A : Type) := (Leaf : t A).
 
-  Fixpoint get (A : Set) (i : positive) (m : t A) {struct i} : option A :=
+  Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
     match m with
     | Leaf => None
     | Node l o r =>
@@ -195,7 +195,7 @@ Module PTree <: TREE.
         end
     end.
 
-  Fixpoint set (A : Set) (i : positive) (v : A) (m : t A) {struct i} : t A :=
+  Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A :=
     match m with
     | Leaf =>
         match i with
@@ -211,7 +211,7 @@ Module PTree <: TREE.
         end
     end.
 
-  Fixpoint remove (A : Set) (i : positive) (m : t A) {struct i} : t A :=
+  Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A :=
     match i with
     | xH =>
         match m with
@@ -242,22 +242,22 @@ Module PTree <: TREE.
     end.
 
   Theorem gempty:
-    forall (A: Set) (i: positive), get i (empty A) = None.
+    forall (A: Type) (i: positive), get i (empty A) = None.
   Proof.
     induction i; simpl; auto.
   Qed.
 
   Theorem gss:
-    forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
+    forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
   Proof.
     induction i; destruct m; simpl; auto.
   Qed.
 
-    Lemma gleaf : forall (A : Set) (i : positive), get i (Leaf : t A) = None.
+    Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None.
     Proof. exact gempty. Qed.
 
   Theorem gso:
-    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    forall (A: Type) (i j: positive) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Proof.
     induction i; intros; destruct j; destruct m; simpl;
@@ -265,7 +265,7 @@ Module PTree <: TREE.
   Qed.
 
   Theorem gsspec:
-    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    forall (A: Type) (i j: positive) (x: A) (m: t A),
     get i (set j x m) = if peq i j then Some x else get i m.
   Proof.
     intros.
@@ -273,7 +273,7 @@ Module PTree <: TREE.
   Qed.
 
   Theorem gsident:
-    forall (A: Set) (i: positive) (m: t A) (v: A),
+    forall (A: Type) (i: positive) (m: t A) (v: A),
     get i m = Some v -> set i v m = m.
   Proof.
     induction i; intros; destruct m; simpl; simpl in H; try congruence.
@@ -281,11 +281,11 @@ Module PTree <: TREE.
      rewrite (IHi m1 v H); congruence.
   Qed.
 
-    Lemma rleaf : forall (A : Set) (i : positive), remove i (Leaf : t A) = Leaf.
+    Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.
     Proof. destruct i; simpl; auto. Qed.
 
   Theorem grs:
-    forall (A: Set) (i: positive) (m: t A), get i (remove i m) = None.
+    forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None.
   Proof.
     induction i; destruct m.
      simpl; auto.
@@ -305,7 +305,7 @@ Module PTree <: TREE.
   Qed.
 
   Theorem gro:
-    forall (A: Set) (i j: positive) (m: t A),
+    forall (A: Type) (i j: positive) (m: t A),
     i <> j -> get i (remove j m) = get i m.
   Proof.
     induction i; intros; destruct j; destruct m;
@@ -335,7 +335,7 @@ Module PTree <: TREE.
 
   Section EXTENSIONAL_EQUALITY.
 
-    Variable A: Set.
+    Variable A: Type.
     Variable eqA: A -> A -> Prop.
     Variable beqA: A -> A -> bool.
     Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
@@ -439,7 +439,7 @@ Module PTree <: TREE.
       simpl; auto.
     Qed.
 
-    Fixpoint xmap (A B : Set) (f : positive -> A -> B) (m : t A) (i : positive)
+    Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive)
              {struct m} : t B :=
       match m with
       | Leaf => Leaf
@@ -448,10 +448,10 @@ Module PTree <: TREE.
                            (xmap f r (append i (xI xH)))
       end.
 
-  Definition map (A B : Set) (f : positive -> A -> B) m := xmap f m xH.
+  Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH.
 
     Lemma xgmap:
-      forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A),
+      forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
       get i (xmap f m j) = option_map (f (append j i)) (get i m).
     Proof.
       induction i; intros; destruct m; simpl; auto.
@@ -461,7 +461,7 @@ Module PTree <: TREE.
     Qed.
 
   Theorem gmap:
-    forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A),
+    forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
     get i (map f m) = option_map (f i) (get i m).
   Proof.
     intros.
@@ -471,7 +471,7 @@ Module PTree <: TREE.
     rewrite append_neutral_l; auto.
   Qed.
 
-    Fixpoint xcombine_l (A : Set) (f : option A -> option A -> option A)
+    Fixpoint xcombine_l (A : Type) (f : option A -> option A -> option A)
                        (m : t A) {struct m} : t A :=
       match m with
       | Leaf => Leaf
@@ -479,14 +479,14 @@ Module PTree <: TREE.
       end.
 
     Lemma xgcombine_l :
-          forall (A : Set) (f : option A -> option A -> option A)
+          forall (A : Type) (f : option A -> option A -> option A)
                  (i : positive) (m : t A),
           f None None = None -> get i (xcombine_l f m) = f (get i m) None.
     Proof.
       induction i; intros; destruct m; simpl; auto.
     Qed.
 
-    Fixpoint xcombine_r (A : Set) (f : option A -> option A -> option A)
+    Fixpoint xcombine_r (A : Type) (f : option A -> option A -> option A)
                        (m : t A) {struct m} : t A :=
       match m with
       | Leaf => Leaf
@@ -494,14 +494,14 @@ Module PTree <: TREE.
       end.
 
     Lemma xgcombine_r :
-          forall (A : Set) (f : option A -> option A -> option A)
+          forall (A : Type) (f : option A -> option A -> option A)
                  (i : positive) (m : t A),
           f None None = None -> get i (xcombine_r f m) = f None (get i m).
     Proof.
       induction i; intros; destruct m; simpl; auto.
     Qed.
 
-  Fixpoint combine (A : Set) (f : option A -> option A -> option A)
+  Fixpoint combine (A : Type) (f : option A -> option A -> option A)
                    (m1 m2 : t A) {struct m1} : t A :=
     match m1 with
     | Leaf => xcombine_r f m2
@@ -513,7 +513,7 @@ Module PTree <: TREE.
     end.
 
     Lemma xgcombine:
-      forall (A: Set) (f: option A -> option A -> option A) (i: positive)
+      forall (A: Type) (f: option A -> option A -> option A) (i: positive)
              (m1 m2: t A),
       f None None = None ->
       get i (combine f m1 m2) = f (get i m1) (get i m2).
@@ -523,7 +523,7 @@ Module PTree <: TREE.
     Qed.
 
   Theorem gcombine:
-    forall (A: Set) (f: option A -> option A -> option A)
+    forall (A: Type) (f: option A -> option A -> option A)
            (m1 m2: t A) (i: positive),
     f None None = None ->
     get i (combine f m1 m2) = f (get i m1) (get i m2).
@@ -532,7 +532,7 @@ Module PTree <: TREE.
   Qed.
 
     Lemma xcombine_lr :
-      forall (A : Set) (f g : option A -> option A -> option A) (m : t A),
+      forall (A : Type) (f g : option A -> option A -> option A) (m : t A),
       (forall (i j : option A), f i j = g j i) ->
       xcombine_l f m = xcombine_r g m.
     Proof.
@@ -543,7 +543,7 @@ Module PTree <: TREE.
     Qed.
 
   Theorem combine_commut:
-    forall (A: Set) (f g: option A -> option A -> option A),
+    forall (A: Type) (f g: option A -> option A -> option A),
     (forall (i j: option A), f i j = g j i) ->
     forall (m1 m2: t A),
     combine f m1 m2 = combine g m2 m1.
@@ -561,7 +561,7 @@ Module PTree <: TREE.
      auto. 
   Qed.
 
-    Fixpoint xelements (A : Set) (m : t A) (i : positive) {struct m}
+    Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m}
              : list (positive * A) :=
       match m with
       | Leaf => nil
@@ -578,7 +578,7 @@ Module PTree <: TREE.
   Definition elements A (m : t A) := xelements m xH.
 
     Lemma xelements_correct:
-      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      forall (A: Type) (m: t A) (i j : positive) (v: A),
       get i m = Some v -> In (append j i, v) (xelements m j).
     Proof.
       induction m; intros.
@@ -595,14 +595,14 @@ Module PTree <: TREE.
     Qed.
 
   Theorem elements_correct:
-    forall (A: Set) (m: t A) (i: positive) (v: A),
+    forall (A: Type) (m: t A) (i: positive) (v: A),
     get i m = Some v -> In (i, v) (elements m).
   Proof.
     intros A m i v H.
     exact (xelements_correct m i xH H).
   Qed.
 
-    Fixpoint xget (A : Set) (i j : positive) (m : t A) {struct j} : option A :=
+    Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
       match i, j with
       | _, xH => get i m
       | xO ii, xO jj => xget ii jj m
@@ -611,7 +611,7 @@ Module PTree <: TREE.
       end.
 
     Lemma xget_left :
-      forall (A : Set) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+      forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
       xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.
     Proof.
       induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
@@ -619,7 +619,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_ii :
-      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      forall (A: Type) (m: t A) (i j : positive) (v: A),
       In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -635,7 +635,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_io :
-      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      forall (A: Type) (m: t A) (i j : positive) (v: A),
       ~In (xI i, v) (xelements m (xO j)).
     Proof.
       induction m.
@@ -650,7 +650,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_oo :
-      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      forall (A: Type) (m: t A) (i j : positive) (v: A),
       In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -666,7 +666,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_oi :
-      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      forall (A: Type) (m: t A) (i j : positive) (v: A),
       ~In (xO i, v) (xelements m (xI j)).
     Proof.
       induction m.
@@ -681,7 +681,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_ih :
-      forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
       In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -694,7 +694,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_oh :
-      forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
       In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -707,7 +707,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_hi :
-      forall (A: Set) (m: t A) (i : positive) (v: A),
+      forall (A: Type) (m: t A) (i : positive) (v: A),
       ~In (xH, v) (xelements m (xI i)).
     Proof.
       induction m; intros.
@@ -722,7 +722,7 @@ Module PTree <: TREE.
     Qed.
 
     Lemma xelements_ho :
-      forall (A: Set) (m: t A) (i : positive) (v: A),
+      forall (A: Type) (m: t A) (i : positive) (v: A),
       ~In (xH, v) (xelements m (xO i)).
     Proof.
       induction m; intros.
@@ -737,13 +737,13 @@ Module PTree <: TREE.
     Qed.
 
     Lemma get_xget_h :
-      forall (A: Set) (m: t A) (i: positive), get i m = xget i xH m.
+      forall (A: Type) (m: t A) (i: positive), get i m = xget i xH m.
     Proof.
       destruct i; simpl; auto.
     Qed.
 
     Lemma xelements_complete:
-      forall (A: Set) (i j : positive) (m: t A) (v: A),
+      forall (A: Type) (i j : positive) (m: t A) (v: A),
       In (i, v) (xelements m j) -> xget i j m = Some v.
     Proof.
       induction i; simpl; intros; destruct j; simpl.
@@ -771,7 +771,7 @@ Module PTree <: TREE.
     Qed.
 
   Theorem elements_complete:
-    forall (A: Set) (m: t A) (i: positive) (v: A),
+    forall (A: Type) (m: t A) (i: positive) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Proof.
     intros A m i v H.
@@ -781,7 +781,7 @@ Module PTree <: TREE.
   Qed.
 
   Lemma in_xelements:
-    forall (A: Set) (m: t A) (i k: positive) (v: A),
+    forall (A: Type) (m: t A) (i k: positive) (v: A),
     In (k, v) (xelements m i) ->
     exists j, k = append i j.
   Proof.
@@ -802,11 +802,11 @@ Module PTree <: TREE.
     rewrite <- append_assoc_1. exists (xI k1); auto.
   Qed.
 
-  Definition xkeys (A: Set) (m: t A) (i: positive) :=
+  Definition xkeys (A: Type) (m: t A) (i: positive) :=
     List.map (@fst positive A) (xelements m i).
 
   Lemma in_xkeys:
-    forall (A: Set) (m: t A) (i k: positive),
+    forall (A: Type) (m: t A) (i k: positive),
     In k (xkeys m i) ->
     exists j, k = append i j.
   Proof.
@@ -816,7 +816,7 @@ Module PTree <: TREE.
   Qed.
 
   Remark list_append_cons_norepet:
-    forall (A: Set) (l1 l2: list A) (x: A),
+    forall (A: Type) (l1 l2: list A) (x: A),
     list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
     ~In x l1 -> ~In x l2 ->
     list_norepet (l1 ++ x :: l2).
@@ -837,7 +837,7 @@ Module PTree <: TREE.
   Qed.
 
   Lemma xelements_keys_norepet:
-    forall (A: Set) (m: t A) (i: positive),
+    forall (A: Type) (m: t A) (i: positive),
     list_norepet (xkeys m i).
   Proof.
     induction m; unfold xkeys; simpl; fold xkeys; intros.
@@ -871,17 +871,17 @@ Module PTree <: TREE.
   Qed.
 
   Theorem elements_keys_norepet:
-    forall (A: Set) (m: t A), 
+    forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
   Proof.
     intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
   Qed.
 
-  Definition fold (A B : Set) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
+  Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
      List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
 
   Theorem fold_spec:
-    forall (A B: Set) (f: B -> positive -> A -> B) (v: B) (m: t A),
+    forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A),
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   Proof.
@@ -896,49 +896,49 @@ Module PMap <: MAP.
   Definition elt := positive.
   Definition elt_eq := peq.
 
-  Definition t (A : Set) : Set := (A * PTree.t A)%type.
+  Definition t (A : Type) : Type := (A * PTree.t A)%type.
 
-  Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+  Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
                  forall (a b: t A), {a = b} + {a <> b}.
   Proof.
     intros. 
-    generalize (PTree.eq H). intros. 
+    generalize (PTree.eq X). intros. 
     decide equality.
   Qed.
 
-  Definition init (A : Set) (x : A) :=
+  Definition init (A : Type) (x : A) :=
     (x, PTree.empty A).
 
-  Definition get (A : Set) (i : positive) (m : t A) :=
+  Definition get (A : Type) (i : positive) (m : t A) :=
     match PTree.get i (snd m) with
     | Some x => x
     | None => fst m
     end.
 
-  Definition set (A : Set) (i : positive) (x : A) (m : t A) :=
+  Definition set (A : Type) (i : positive) (x : A) (m : t A) :=
     (fst m, PTree.set i x (snd m)).
 
   Theorem gi:
-    forall (A: Set) (i: positive) (x: A), get i (init x) = x.
+    forall (A: Type) (i: positive) (x: A), get i (init x) = x.
   Proof.
     intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto.
   Qed.
 
   Theorem gss:
-    forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
+    forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
   Proof.
     intros. unfold get. unfold set. simpl. rewrite PTree.gss. auto.
   Qed.
 
   Theorem gso:
-    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    forall (A: Type) (i j: positive) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Proof.
     intros. unfold get. unfold set. simpl. rewrite PTree.gso; auto.
   Qed.
 
   Theorem gsspec:
-    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    forall (A: Type) (i j: positive) (x: A) (m: t A),
     get i (set j x m) = if peq i j then x else get i m.
   Proof.
     intros. destruct (peq i j).
@@ -947,7 +947,7 @@ Module PMap <: MAP.
   Qed.
 
   Theorem gsident:
-    forall (A: Set) (i j: positive) (m: t A),
+    forall (A: Type) (i j: positive) (m: t A),
     get j (set i (get i m) m) = get j m.
   Proof.
     intros. destruct (peq i j).
@@ -955,11 +955,11 @@ Module PMap <: MAP.
      rewrite gso; auto.
   Qed.
 
-  Definition map (A B : Set) (f : A -> B) (m : t A) : t B :=
+  Definition map (A B : Type) (f : A -> B) (m : t A) : t B :=
     (f (fst m), PTree.map (fun _ => f) (snd m)).
 
   Theorem gmap:
-    forall (A B: Set) (f: A -> B) (i: positive) (m: t A),
+    forall (A B: Type) (f: A -> B) (i: positive) (m: t A),
     get i (map f m) = f(get i m).
   Proof.
     intros. unfold map. unfold get. simpl. rewrite PTree.gmap.
@@ -971,7 +971,7 @@ End PMap.
 (** * An implementation of maps over any type that injects into type [positive] *)
 
 Module Type INDEXED_TYPE.
-  Variable t: Set.
+  Variable t: Type.
   Variable index: t -> positive.
   Hypothesis index_inj: forall (x y: t), index x = index y -> x = y.
   Variable eq: forall (x y: t), {x = y} + {x <> y}.
@@ -981,28 +981,28 @@ Module IMap(X: INDEXED_TYPE).
 
   Definition elt := X.t.
   Definition elt_eq := X.eq.
-  Definition t : Set -> Set := PMap.t.
-  Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+  Definition t : Type -> Type := PMap.t.
+  Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
                  forall (a b: t A), {a = b} + {a <> b} := PMap.eq.
-  Definition init (A: Set) (x: A) := PMap.init x.
-  Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m.
-  Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
-  Definition map (A B: Set) (f: A -> B) (m: t A) : t B := PMap.map f m.
+  Definition init (A: Type) (x: A) := PMap.init x.
+  Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.
+  Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
+  Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m.
 
   Lemma gi:
-    forall (A: Set) (x: A) (i: X.t), get i (init x) = x.
+    forall (A: Type) (x: A) (i: X.t), get i (init x) = x.
   Proof.
     intros. unfold get, init. apply PMap.gi. 
   Qed.
 
   Lemma gss:
-    forall (A: Set) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
+    forall (A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
   Proof.
     intros. unfold get, set. apply PMap.gss.
   Qed.
 
   Lemma gso:
-    forall (A: Set) (i j: X.t) (x: A) (m: t A),
+    forall (A: Type) (i j: X.t) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Proof.
     intros. unfold get, set. apply PMap.gso. 
@@ -1010,7 +1010,7 @@ Module IMap(X: INDEXED_TYPE).
   Qed.
 
   Lemma gsspec:
-    forall (A: Set) (i j: X.t) (x: A) (m: t A),
+    forall (A: Type) (i j: X.t) (x: A) (m: t A),
     get i (set j x m) = if X.eq i j then x else get i m.
   Proof.
     intros. unfold get, set. 
@@ -1022,7 +1022,7 @@ Module IMap(X: INDEXED_TYPE).
   Qed.
 
   Lemma gmap:
-    forall (A B: Set) (f: A -> B) (i: X.t) (m: t A),
+    forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),
     get i (map f m) = f(get i m).
   Proof.
     intros. unfold map, get. apply PMap.gmap. 
@@ -1074,7 +1074,7 @@ Module NMap := IMap(NIndexed).
 (** * An implementation of maps over any type with decidable equality *)
 
 Module Type EQUALITY_TYPE.
-  Variable t: Set.
+  Variable t: Type.
   Variable eq: forall (x y: t), {x = y} + {x <> y}.
 End EQUALITY_TYPE.
 
@@ -1082,45 +1082,45 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
 
   Definition elt := X.t.
   Definition elt_eq := X.eq.
-  Definition t (A: Set) := X.t -> A.
-  Definition init (A: Set) (v: A) := fun (_: X.t) => v.
-  Definition get (A: Set) (x: X.t) (m: t A) := m x.
-  Definition set (A: Set) (x: X.t) (v: A) (m: t A) :=
+  Definition t (A: Type) := X.t -> A.
+  Definition init (A: Type) (v: A) := fun (_: X.t) => v.
+  Definition get (A: Type) (x: X.t) (m: t A) := m x.
+  Definition set (A: Type) (x: X.t) (v: A) (m: t A) :=
     fun (y: X.t) => if X.eq y x then v else m y.
   Lemma gi:
-    forall (A: Set) (i: elt) (x: A), init x i = x.
+    forall (A: Type) (i: elt) (x: A), init x i = x.
   Proof.
     intros. reflexivity.
   Qed.
   Lemma gss:
-    forall (A: Set) (i: elt) (x: A) (m: t A), (set i x m) i = x.
+    forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
   Proof.
     intros. unfold set. case (X.eq i i); intro.
     reflexivity. tauto.
   Qed.
   Lemma gso:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     i <> j -> (set j x m) i = m i.
   Proof.
     intros. unfold set. case (X.eq i j); intro.
     congruence. reflexivity.
   Qed.
   Lemma gsspec:
-    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then x else get i m.
   Proof.
     intros. unfold get, set, elt_eq. reflexivity.
   Qed.
   Lemma gsident:
-    forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+    forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
   Proof.
     intros. unfold get, set. case (X.eq j i); intro.
     congruence. reflexivity.
   Qed.
-  Definition map (A B: Set) (f: A -> B) (m: t A) :=
+  Definition map (A B: Type) (f: A -> B) (m: t A) :=
     fun (x: X.t) => f(m x).
   Lemma gmap:
-    forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
     get i (map f m) = f(get i m).
   Proof.
     intros. unfold get, map. reflexivity.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index 4b1f4e0f..eddc3721 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -45,6 +45,8 @@ Proof.
   assert (Zpos x <> Zpos y). congruence. omega.
 Qed.
 
+Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
+
 End OrderedPositive.
 
 (** Indexed types (those that inject into [positive]) are ordered. *)
@@ -81,6 +83,13 @@ Proof.
   apply GT. exact l.
 Qed.
 
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+  intros. case (peq (A.index x) (A.index y)); intros.
+  left. apply A.index_inj; auto.
+  right; red; unfold eq; intros; subst. congruence. 
+Qed.
+
 End OrderedIndexed.
 
 (** The product of two ordered types is ordered. *)
@@ -164,5 +173,15 @@ Proof.
   apply GT. red. left. auto.
 Qed.
 
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+  unfold eq; intros.
+  case (A.eq_dec (fst x) (fst y)); intros.
+  case (B.eq_dec (snd x) (snd y)); intros.
+  left; auto.
+  right; intuition.
+  right; intuition.
+Qed.
+
 End OrderedPair.
 
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 2c7b82a7..edb267e4 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -63,7 +63,7 @@ Section PARMOV.
 (** The development is parameterized by the type of registers, 
     equipped with a decidable equality. *)
 
-Variable reg: Set.
+Variable reg: Type.
 Variable reg_eq : forall (r1 r2: reg), {r1=r2} + {r1<>r2}.
 
 (** The [temp] function maps every register [r] to the register that
@@ -93,7 +93,7 @@ Definition dests (m: moves) := List.map (@snd reg reg) m.
 (** The dynamic  semantics of moves is given in terms of environments.
     An environment is a mapping of registers to their current values. *)
 
-Variable val: Set.
+Variable val: Type.
 Definition env := reg -> val.
 
 Lemma env_ext:
@@ -186,7 +186,7 @@ Fixpoint exec_seq_rev (m: moves) (e: env) {struct m}: env :=
    as an inductive predicate [transition] relating triples of moves,
    and its reflexive transitive closure [transitions]. *)
 
-Inductive state: Set :=
+Inductive state: Type :=
   State (mu: moves) (sigma: moves) (tau: moves) : state.
 
 Definition no_read (mu: moves) (d: reg) : Prop :=
@@ -1331,7 +1331,7 @@ Qed.
 
 Section REGISTER_CLASSES.
 
-Variable class: Set.
+Variable class: Type.
 Variable regclass: reg -> class.
 Hypothesis temp_preserves_class: forall r, regclass (temp r) = regclass r.
 
-- 
cgit