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

8 files changed, 107 insertions, 107 deletions

diff --git a/common/AST.v b/common/AST.v
index ec8053d..a8655c2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -36,7 +36,7 @@ Definition ident_eq := peq.
   [Tint] for integers and pointers, and [Tfloat] for floating-point
   numbers. *)
 
-Inductive typ : Set :=
+Inductive typ : Type :=
   | Tint : typ
   | Tfloat : typ.
 
@@ -58,7 +58,7 @@ Proof. decide equality. apply typ_eq. Qed.
   are used in particular to determine appropriate calling conventions
   for the function. *)
 
-Record signature : Set := mksignature {
+Record signature : Type := mksignature {
   sig_args: list typ;
   sig_res: option typ
 }.
@@ -73,7 +73,7 @@ Definition proj_sig_res (s: signature) : typ :=
   a ``memory chunk'' indicating the type, size and signedness of the
   chunk of memory being accessed. *)
 
-Inductive memory_chunk : Set :=
+Inductive memory_chunk : Type :=
   | Mint8signed : memory_chunk     (**r 8-bit signed integer *)
   | Mint8unsigned : memory_chunk   (**r 8-bit unsigned integer *)
   | Mint16signed : memory_chunk    (**r 16-bit signed integer *)
@@ -84,7 +84,7 @@ Inductive memory_chunk : Set :=
 
 (** Initialization data for global variables. *)
 
-Inductive init_data: Set :=
+Inductive init_data: Type :=
   | Init_int8: int -> init_data
   | Init_int16: int -> init_data
   | Init_int32: int -> init_data
@@ -104,16 +104,16 @@ for variables vary among the various intermediate languages and are
 taken as parameters to the [program] type.  The other parts of whole
 programs are common to all languages. *)
 
-Record program (F V: Set) : Set := mkprogram {
+Record program (F V: Type) : Type := mkprogram {
   prog_funct: list (ident * F);
   prog_main: ident;
   prog_vars: list (ident * list init_data * V)
 }.
 
-Definition prog_funct_names (F V: Set) (p: program F V) : list ident :=
+Definition prog_funct_names (F V: Type) (p: program F V) : list ident :=
   map (@fst ident F) p.(prog_funct).
 
-Definition prog_var_names (F V: Set) (p: program F V) : list ident :=
+Definition prog_var_names (F V: Type) (p: program F V) : list ident :=
   map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars).
 
 (** * Generic transformations over programs *)
@@ -124,7 +124,7 @@ Definition prog_var_names (F V: Set) (p: program F V) : list ident :=
 
 Section TRANSF_PROGRAM.
 
-Variable A B V: Set.
+Variable A B V: Type.
 Variable transf: A -> B.
 
 Definition transf_program (l: list (ident * A)) : list (ident * B) :=
@@ -158,7 +158,7 @@ Open Local Scope string_scope.
 
 Section MAP_PARTIAL.
 
-Variable A B C: Set.
+Variable A B C: Type.
 Variable prefix_errmsg: A -> errmsg.
 Variable f: B -> res C.
 
@@ -207,7 +207,7 @@ Qed.
 End MAP_PARTIAL.
 
 Remark map_partial_total:
-  forall (A B C: Set) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
+  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
   map_partial prefix (fun b => OK (f b)) l =
   OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
 Proof.
@@ -217,7 +217,7 @@ Proof.
 Qed.
 
 Remark map_partial_identity:
-  forall (A B: Set) (prefix: A -> errmsg) (l: list (A * B)),
+  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
   map_partial prefix (fun b => OK b) l = OK l.
 Proof.
   induction l; simpl.
@@ -227,7 +227,7 @@ Qed.
 
 Section TRANSF_PARTIAL_PROGRAM.
 
-Variable A B V: Set.
+Variable A B V: Type.
 Variable transf_partial: A -> res B.
 
 Definition prefix_funct_name (id: ident) : errmsg :=
@@ -271,7 +271,7 @@ End TRANSF_PARTIAL_PROGRAM.
 
 Section TRANSF_PARTIAL_PROGRAM2.
 
-Variable A B V W: Set.
+Variable A B V W: Type.
 Variable transf_partial_function: A -> res B.
 Variable transf_partial_variable: V -> res W.
 
@@ -322,7 +322,7 @@ End TRANSF_PARTIAL_PROGRAM2.
 
 Section MATCH_PROGRAM.
 
-Variable A B V W: Set.
+Variable A B V W: Type.
 Variable match_fundef: A -> B -> Prop.
 Variable match_varinfo: V -> W -> Prop.
 
@@ -344,7 +344,7 @@ Definition match_program (p1: program A V) (p2: program B W) : Prop :=
 End MATCH_PROGRAM.
 
 Remark transform_partial_program2_match:
-  forall (A B V W: Set)
+  forall (A B V W: Type)
          (transf_partial_function: A -> res B)
          (transf_partial_variable: V -> res W)
          (p: program A V) (tp: program B W),
@@ -375,12 +375,12 @@ Qed.
   (a.k.a. system calls) that emit an event when applied.  We define
   a type for such functions and some generic transformation functions. *)
 
-Record external_function : Set := mkextfun {
+Record external_function : Type := mkextfun {
   ef_id: ident;
   ef_sig: signature
 }.
 
-Inductive fundef (F: Set): Set :=
+Inductive fundef (F: Type): Type :=
   | Internal: F -> fundef F
   | External: external_function -> fundef F.
 
@@ -388,7 +388,7 @@ Implicit Arguments External [F].
 
 Section TRANSF_FUNDEF.
 
-Variable A B: Set.
+Variable A B: Type.
 Variable transf: A -> B.
 
 Definition transf_fundef (fd: fundef A): fundef B :=
@@ -401,7 +401,7 @@ End TRANSF_FUNDEF.
 
 Section TRANSF_PARTIAL_FUNDEF.
 
-Variable A B: Set.
+Variable A B: Type.
 Variable transf_partial: A -> res B.
 
 Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
diff --git a/common/Errors.v b/common/Errors.v
index 2c9bbc3..2165db3 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -28,11 +28,11 @@ Set Implicit Arguments.
   as a list of either substrings or positive numbers encoding
   a source-level identifier (see module AST). *)
 
-Inductive errcode: Set :=
+Inductive errcode: Type :=
   | MSG: string -> errcode
   | CTX: positive -> errcode.
 
-Definition errmsg: Set := list errcode.
+Definition errmsg: Type := list errcode.
 
 Definition msg (s: string) : errmsg := MSG s :: nil.
 
@@ -42,7 +42,7 @@ Definition msg (s: string) : errmsg := MSG s :: nil.
   The return value is either [OK res] to indicate success,
   or [Error msg] to indicate failure. *)
 
-Inductive res (A: Set) : Set :=
+Inductive res (A: Type) : Type :=
 | OK: A -> res A
 | Error: errmsg -> res A.
 
@@ -51,13 +51,13 @@ Implicit Arguments Error [A].
 (** To automate the propagation of errors, we use a monadic style
   with the following [bind] operation. *)
 
-Definition bind (A B: Set) (f: res A) (g: A -> res B) : res B :=
+Definition bind (A B: Type) (f: res A) (g: A -> res B) : res B :=
   match f with
   | OK x => g x
   | Error msg => Error msg
   end.
 
-Definition bind2 (A B C: Set) (f: res (A * B)) (g: A -> B -> res C) : res C :=
+Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C :=
   match f with
   | OK (x, y) => g x y
   | Error msg => Error msg
@@ -74,7 +74,7 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
  : error_monad_scope.
 
 Remark bind_inversion:
-  forall (A B: Set) (f: res A) (g: A -> res B) (y: B),
+  forall (A B: Type) (f: res A) (g: A -> res B) (y: B),
   bind f g = OK y ->
   exists x, f = OK x /\ g x = OK y.
 Proof.
@@ -84,7 +84,7 @@ Proof.
 Qed.
 
 Remark bind2_inversion:
-  forall (A B C: Set) (f: res (A*B)) (g: A -> B -> res C) (z: C),
+  forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C),
   bind2 f g = OK z ->
   exists x, exists y, f = OK (x, y) /\ g x y = OK z.
 Proof.
@@ -97,14 +97,14 @@ Open Local Scope error_monad_scope.
 
 (** This is the familiar monadic map iterator. *)
 
-Fixpoint mmap (A B: Set) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
+Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
   match l with
   | nil => OK nil
   | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
   end.
 
 Remark mmap_inversion:
-  forall (A B: Set) (f: A -> res B) (l: list A) (l': list B),
+  forall (A B: Type) (f: A -> res B) (l: list A) (l': list B),
   mmap f l = OK l' ->
   list_forall2 (fun x y => f x = OK y) l l'.
 Proof.
diff --git a/common/Events.v b/common/Events.v
index c44da01..011c454 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -32,11 +32,11 @@ Require Import Values.
   allow pointers to be exchanged between the program and the outside
   world. *)
 
-Inductive eventval: Set :=
+Inductive eventval: Type :=
   | EVint: int -> eventval
   | EVfloat: float -> eventval.
 
-Record event : Set := mkevent {
+Record event : Type := mkevent {
   ev_name: ident;
   ev_args: list eventval;
   ev_res: eventval
@@ -56,7 +56,7 @@ Definition Eextcall
 
 Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.
 
-CoInductive traceinf : Set :=
+CoInductive traceinf : Type :=
   | Enilinf: traceinf
   | Econsinf: event -> traceinf -> traceinf.
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index f720914..1ce7bf5 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -47,43 +47,43 @@ Module Type GENV.
 
 (** ** Types and operations *)
 
-  Variable t: Set -> Set.
+  Variable t: Type -> Type.
    (** The type of global environments.  The parameter [F] is the type
        of function descriptions. *)
 
-  Variable globalenv: forall (F V: Set), program F V -> t F.
+  Variable globalenv: forall (F V: Type), program F V -> t F.
    (** Return the global environment for the given program. *)
 
-  Variable init_mem: forall (F V: Set), program F V -> mem.
+  Variable init_mem: forall (F V: Type), program F V -> mem.
    (** Return the initial memory state for the given program. *)
 
-  Variable find_funct_ptr: forall (F: Set), t F -> block -> option F.
+  Variable find_funct_ptr: forall (F: Type), t F -> block -> option F.
    (** Return the function description associated with the given address,
        if any. *)
 
-  Variable find_funct: forall (F: Set), t F -> val -> option F.
+  Variable find_funct: forall (F: Type), t F -> val -> option F.
    (** Same as [find_funct_ptr] but the function address is given as
        a value, which must be a pointer with offset 0. *)
 
-  Variable find_symbol: forall (F: Set), t F -> ident -> option block.
+  Variable find_symbol: forall (F: Type), t F -> ident -> option block.
    (** Return the address of the given global symbol, if any. *)
 
 (** ** Properties of the operations. *)
 
   Hypothesis find_funct_inv:
-    forall (F: Set) (ge: t F) (v: val) (f: F),
+    forall (F: Type) (ge: t F) (v: val) (f: F),
     find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.
   Hypothesis find_funct_find_funct_ptr:
-    forall (F: Set) (ge: t F) (b: block),
+    forall (F: Type) (ge: t F) (b: block),
     find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.    
 
   Hypothesis find_symbol_exists:
-    forall (F V: Set) (p: program F V)
+    forall (F V: Type) (p: program F V)
            (id: ident) (init: list init_data) (v: V),
     In (id, init, v) (prog_vars p) ->
     exists b, find_symbol (globalenv p) id = Some b.
   Hypothesis find_funct_ptr_exists:
-    forall (F V: Set) (p: program F V) (id: ident) (f: F),
+    forall (F V: Type) (p: program F V) (id: ident) (f: F),
     list_norepet (prog_funct_names p) ->
     list_disjoint (prog_funct_names p) (prog_var_names p) ->
     In (id, f) (prog_funct p) ->
@@ -91,49 +91,49 @@ Module Type GENV.
            /\ find_funct_ptr (globalenv p) b = Some f.
 
   Hypothesis find_funct_ptr_inversion:
-    forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
+    forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F),
     find_funct_ptr (globalenv p) b = Some f ->
     exists id, In (id, f) (prog_funct p).
   Hypothesis find_funct_inversion:
-    forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
+    forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F),
     find_funct (globalenv p) v = Some f ->
     exists id, In (id, f) (prog_funct p).
   Hypothesis find_funct_ptr_symbol_inversion:
-    forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F),
+    forall (F V: Type) (p: program F V) (id: ident) (b: block) (f: F),
     find_symbol (globalenv p) id = Some b ->
     find_funct_ptr (globalenv p) b = Some f ->
     In (id, f) p.(prog_funct).
 
   Hypothesis find_funct_ptr_prop:
-    forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
+    forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F),
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
     find_funct_ptr (globalenv p) b = Some f ->
     P f.
   Hypothesis find_funct_prop:
-    forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
+    forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F),
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
     find_funct (globalenv p) v = Some f ->
     P f.
 
   Hypothesis initmem_nullptr:
-    forall (F V: Set) (p: program F V),
+    forall (F V: Type) (p: program F V),
     let m := init_mem p in
     valid_block m nullptr /\
     m.(blocks) nullptr = empty_block 0 0.
   Hypothesis initmem_inject_neutral:
-    forall (F V: Set) (p: program F V),
+    forall (F V: Type) (p: program F V),
     mem_inject_neutral (init_mem p).
   Hypothesis find_funct_ptr_negative:
-    forall (F V: Set) (p: program F V) (b: block) (f: F),
+    forall (F V: Type) (p: program F V) (b: block) (f: F),
     find_funct_ptr (globalenv p) b = Some f -> b < 0.
   Hypothesis find_symbol_not_fresh:
-    forall (F V: Set) (p: program F V) (id: ident) (b: block),
+    forall (F V: Type) (p: program F V) (id: ident) (b: block),
     find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).
   Hypothesis find_symbol_not_nullptr:
-    forall (F V: Set) (p: program F V) (id: ident) (b: block),
+    forall (F V: Type) (p: program F V) (id: ident) (b: block),
     find_symbol (globalenv p) id = Some b -> b <> nullptr.
   Hypothesis global_addresses_distinct:
-    forall (F V: Set) (p: program F V) id1 id2 b1 b2,
+    forall (F V: Type) (p: program F V) id1 id2 b1 b2,
     id1<>id2 ->
     find_symbol (globalenv p) id1 = Some b1 ->
     find_symbol (globalenv p) id2 = Some b2 ->
@@ -143,30 +143,30 @@ Module Type GENV.
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
     find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f).
   Hypothesis find_funct_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
     find_funct (globalenv (transform_program transf p)) v = Some (transf f).
   Hypothesis find_symbol_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     forall (s: ident),
     find_symbol (globalenv (transform_program transf p)) s =
     find_symbol (globalenv p) s.
   Hypothesis init_mem_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     init_mem (transform_program transf p) = init_mem p.
   Hypothesis find_funct_ptr_rev_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     forall (b : block) (tf : B),
     find_funct_ptr (globalenv (transform_program transf p)) b = Some tf ->
     exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.
   Hypothesis find_funct_rev_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (A B V: Type) (transf: A -> B) (p: program A V),
     forall (v : val) (tf : B),
     find_funct (globalenv (transform_program transf p)) v = Some tf ->
     exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf.
@@ -175,37 +175,37 @@ Module Type GENV.
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
     exists f',
     find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
   Hypothesis find_funct_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
     exists f',
     find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
   Hypothesis find_symbol_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     forall (s: ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     init_mem p' = init_mem p.
   Hypothesis find_funct_ptr_rev_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     forall (b : block) (tf : B),
     find_funct_ptr (globalenv p') b = Some tf ->
     exists f : A,
       find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
   Hypothesis find_funct_rev_transf_partial:
-    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),
     transform_partial_program transf p = OK p' ->
     forall (v : val) (tf : B),
     find_funct (globalenv p') v = Some tf ->
@@ -213,7 +213,7 @@ Module Type GENV.
       find_funct (globalenv p) v = Some f /\ transf f = OK tf.
 
   Hypothesis find_funct_ptr_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (b: block) (f: A),
@@ -221,7 +221,7 @@ Module Type GENV.
     exists f',
     find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
   Hypothesis find_funct_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (v: val) (f: A),
@@ -229,18 +229,18 @@ Module Type GENV.
     exists f',
     find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
   Hypothesis find_symbol_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (s: ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     init_mem p' = init_mem p.
   Hypothesis find_funct_ptr_rev_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (b : block) (tf : B),
@@ -248,7 +248,7 @@ Module Type GENV.
     exists f : A,
       find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
   Hypothesis find_funct_rev_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
     transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (v : val) (tf : B),
@@ -260,7 +260,7 @@ Module Type GENV.
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     forall (b : block) (f : A),
@@ -268,7 +268,7 @@ Module Type GENV.
     exists tf : B,
     find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.
   Hypothesis find_funct_ptr_rev_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     forall (b : block) (tf : B),
@@ -276,27 +276,27 @@ Module Type GENV.
     exists f : A,
     find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.
   Hypothesis find_funct_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     forall (v : val) (f : A),
     find_funct (globalenv p) v = Some f ->
     exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf.
   Hypothesis find_funct_rev_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     forall (v : val) (tf : B),
     find_funct (globalenv p') v = Some tf ->
     exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf.
   Hypothesis find_symbol_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     forall (s : ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_match:
-    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+    forall (A B V W: Type) (match_fun: A -> B -> Prop)
            (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
     match_program match_fun match_var p p' ->
     init_mem p' = init_mem p.
@@ -310,10 +310,10 @@ Module Genv: GENV.
 
 Section GENV.
 
-Variable F: Set.                    (* The type of functions *)
-Variable V: Set.                    (* The type of information over variables *)
+Variable F: Type.                    (* The type of functions *)
+Variable V: Type.                    (* The type of information over variables *)
 
-Record genv : Set := mkgenv {
+Record genv : Type := mkgenv {
   functions: ZMap.t (option F);     (* mapping function ptr -> function *)
   nextfunction: Z;
   symbols: PTree.t block                (* mapping symbol -> block *)
@@ -588,7 +588,7 @@ Proof.
   generalize (find_symbol_above_nextfunction _ _ X).
   unfold block; unfold ZIndexed.t; intro; omega.
 
-  intros. exploit H; eauto. assumption. intros [b [X Y]].
+  intros. exploit H; eauto. intros [b [X Y]].
   exists b; split.
   unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. 
   assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. 
@@ -770,7 +770,7 @@ End GENV.
 
 Section MATCH_PROGRAM.
 
-Variable A B V W: Set.
+Variable A B V W: Type.
 Variable match_fun: A -> B -> Prop.
 Variable match_var: V -> W -> Prop.
 Variable p: program A V.
@@ -950,7 +950,7 @@ End MATCH_PROGRAM.
 
 Section TRANSF_PROGRAM_PARTIAL2.
 
-Variable A B V W: Set.
+Variable A B V W: Type.
 Variable transf_fun: A -> res B.
 Variable transf_var: V -> res W.
 Variable p: program A V.
@@ -1024,7 +1024,7 @@ End TRANSF_PROGRAM_PARTIAL2.
 
 Section TRANSF_PROGRAM_PARTIAL.
 
-Variable A B V: Set.
+Variable A B V: Type.
 Variable transf: A -> res B.
 Variable p: program A V.
 Variable p': program B V.
@@ -1089,7 +1089,7 @@ End TRANSF_PROGRAM_PARTIAL.
 
 Section TRANSF_PROGRAM.
 
-Variable A B V: Set.
+Variable A B V: Type.
 Variable transf: A -> B.
 Variable p: program A V.
 Let tp := transform_program transf p.
diff --git a/common/Mem.v b/common/Mem.v
index e169dfc..01c1975 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -31,20 +31,20 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 
-Definition update (A: Set) (x: Z) (v: A) (f: Z -> A) : Z -> A :=
+Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A :=
   fun y => if zeq y x then v else f y.
 
 Implicit Arguments update [A].
 
 Lemma update_s:
-  forall (A: Set) (x: Z) (v: A) (f: Z -> A),
+  forall (A: Type) (x: Z) (v: A) (f: Z -> A),
   update x v f x = v.
 Proof.
   intros; unfold update. apply zeq_true.
 Qed.
 
 Lemma update_o:
-  forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z),
+  forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z),
   x <> y -> update x v f y = f y.
 Proof.
   intros; unfold update. apply zeq_false; auto.
@@ -62,17 +62,17 @@ Qed.
   [d+2] and [d+3].  The [Cont] contents enable detecting future writes
   that would partially overlap the 4-byte value. *)
 
-Inductive content : Set :=
+Inductive content : Type :=
   | Undef: content                 (**r undefined contents *)
   | Datum: nat -> val -> content   (**r first byte of a value *)
   | Cont: content.          (**r continuation bytes for a multi-byte value *)
 
-Definition contentmap : Set := Z -> content.
+Definition contentmap : Type := Z -> content.
 
 (** A memory block comprises the dimensions of the block (low and high bounds)
   plus a mapping from byte offsets to contents.  *)
 
-Record block_contents : Set := mkblock {
+Record block_contents : Type := mkblock {
   low: Z;
   high: Z;
   contents: contentmap
@@ -82,7 +82,7 @@ Record block_contents : Set := mkblock {
   integers) to blocks.  We also maintain the address of the next 
   unallocated block, and a proof that this address is positive. *)
 
-Record mem : Set := mkmem {
+Record mem : Type := mkmem {
   blocks: Z -> block_contents;
   nextblock: block;
   nextblock_pos: nextblock > 0
@@ -455,7 +455,7 @@ Proof.
 Defined.
 
 Lemma in_bounds_true:
-  forall m chunk b ofs (A: Set) (a1 a2: A),
+  forall m chunk b ofs (A: Type) (a1 a2: A),
   valid_access m chunk b ofs ->
   (if in_bounds m chunk b ofs then a1 else a2) = a1.
 Proof.
@@ -858,7 +858,7 @@ Qed.
 
 Inductive load_store_cases 
       (chunk1: memory_chunk) (b1: block) (ofs1: Z)
-      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Set :=
+      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type :=
   | lsc_similar:
       b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 ->
       load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
@@ -1277,7 +1277,7 @@ Qed.
 
 Section GENERIC_INJECT.
 
-Definition meminj : Set := block -> option (block * Z).
+Definition meminj : Type := block -> option (block * Z).
 
 Variable val_inj: meminj -> val -> val -> Prop.
 
@@ -2838,7 +2838,7 @@ Qed.
 (** Signed 8- and 16-bit stores can be performed like unsigned stores. *)
 
 Remark in_bounds_equiv:
-  forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A),
+  forall chunk1 chunk2 m b ofs (A: Type) (a1 a2: A),
   size_chunk chunk1 = size_chunk chunk2 ->
   (if in_bounds m chunk1 b ofs then a1 else a2) =
   (if in_bounds m chunk2 b ofs then a1 else a2).
diff --git a/common/Smallstep.v b/common/Smallstep.v
index a2634be..f41fe4e 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -33,8 +33,8 @@ Set Implicit Arguments.
 
 Section CLOSURES.
 
-Variable genv: Set.
-Variable state: Set.
+Variable genv: Type.
+Variable state: Type.
 
 (** A one-step transition relation has the following signature.
   It is parameterized by a global environment, which does not
@@ -197,7 +197,7 @@ Qed.
 (** An alternate, equivalent definition of [forever] that is useful
     for coinductive reasoning. *)
 
-Variable A: Set.
+Variable A: Type.
 Variable order: A -> A -> Prop.
 
 CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop :=
@@ -290,7 +290,7 @@ Qed.
    finite prefix of this trace, or the whole trace.)
 *)
 
-Inductive program_behavior: Set :=
+Inductive program_behavior: Type :=
   | Terminates: trace -> int -> program_behavior
   | Diverges: traceinf -> program_behavior.
 
@@ -326,8 +326,8 @@ Section SIMULATION.
 
 (** The first small-step semantics is axiomatized as follows. *)
 
-Variable genv1: Set.
-Variable state1: Set.
+Variable genv1: Type.
+Variable state1: Type.
 Variable step1: genv1 -> state1 -> trace -> state1 -> Prop.
 Variable initial_state1: state1 -> Prop.
 Variable final_state1: state1 -> int -> Prop.
@@ -335,8 +335,8 @@ Variable ge1: genv1.
 
 (** The second small-step semantics is also axiomatized. *)
 
-Variable genv2: Set.
-Variable state2: Set.
+Variable genv2: Type.
+Variable state2: Type.
 Variable step2: genv2 -> state2 -> trace -> state2 -> Prop.
 Variable initial_state2: state2 -> Prop.
 Variable final_state2: state2 -> int -> Prop.
diff --git a/common/Switch.v b/common/Switch.v
index 8124aea..179d4d2 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -23,7 +23,7 @@ Require Import Integers.
 (** A multi-way branch is composed of a list of (key, action) pairs,
   plus a default action.  *)
 
-Definition table : Set := list (int * nat).
+Definition table : Type := list (int * nat).
 
 Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
                        {struct cases} : nat :=
@@ -37,7 +37,7 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
     Each node of the tree performs an equality test or a less-than
     test against one of the keys. *)
 
-Inductive comptree : Set :=
+Inductive comptree : Type :=
   | CTaction: nat -> comptree
   | CTifeq: int -> nat -> comptree -> comptree
   | CTiflt: int -> comptree -> comptree -> comptree.
diff --git a/common/Values.v b/common/Values.v
index 8182d7a..9645e8a 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -21,7 +21,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 
-Definition block : Set := Z.
+Definition block : Type := Z.
 Definition eq_block := zeq.
 
 (** A value is either:
@@ -33,7 +33,7 @@ Definition eq_block := zeq.
   value of an uninitialized variable.
 *)
 
-Inductive val: Set :=
+Inductive val: Type :=
   | Vundef: val
   | Vint: int -> val
   | Vfloat: float -> val