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

26 files changed, 168 insertions, 229 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3971fb6..e2387b5 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -167,7 +167,7 @@ Proof.
   eapply DS.fixpoint_solution. unfold analyze in H; eauto.
   auto. auto. auto. auto.
   unfold transfer. rewrite H3.
-  red; intros. elim (Regset.empty_1 _ H4).
+  red; intros. elim (Regset.empty_1 H4).
   unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
 Qed.
 
@@ -581,7 +581,7 @@ Proof.
   rewrite H. simpl. 
   caseEq (Regset.mem res live!!pc); intro LV;
   rewrite LV in AG.
-  generalize (Regset.mem_2 _ _ LV). intro LV'.
+  generalize (Regset.mem_2 LV). intro LV'.
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
   unfold correct_alloc_instr, is_redundant_move.
   caseEq (is_move_operation op args).
diff --git a/backend/Bounds.v b/backend/Bounds.v
index d1ed28d..8c5f536 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -30,7 +30,7 @@ Require Import Conventions.
   These properties are used later to reason about the layout of
   the activation record. *)
 
-Record bounds : Set := mkbounds {
+Record bounds : Type := mkbounds {
   bound_int_local: Z;
   bound_float_local: Z;
   bound_int_callee_save: Z;
@@ -116,7 +116,7 @@ Definition slots_of_instr (i: instruction) : list slot :=
   | _ => nil
   end.
 
-Definition max_over_list (A: Set) (valu: A -> Z) (l: list A) : Z :=
+Definition max_over_list (A: Type) (valu: A -> Z) (l: list A) : Z :=
   List.fold_left (fun m l => Zmax m (valu l)) l 0.
 
 Definition max_over_instrs (valu: instruction -> Z) : Z :=
@@ -151,7 +151,7 @@ Definition outgoing_space (i: instruction) :=
   match i with Lcall sig _ => size_arguments sig | _ => 0 end.
 
 Lemma max_over_list_pos:
-  forall (A: Set) (valu: A -> Z) (l: list A),
+  forall (A: Type) (valu: A -> Z) (l: list A),
   max_over_list A valu l >= 0.
 Proof.
   intros until valu. unfold max_over_list.
@@ -196,7 +196,7 @@ Qed.
 (** We now show the correctness of the inferred bounds. *)
 
 Lemma max_over_list_bound:
-  forall (A: Set) (valu: A -> Z) (l: list A) (x: A),
+  forall (A: Type) (valu: A -> Z) (l: list A) (x: A),
   In x l -> valu x <= max_over_list A valu l.
 Proof.
   intros until x. unfold max_over_list.
diff --git a/backend/CSE.v b/backend/CSE.v
index 13e9be8..cad3503 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -49,7 +49,7 @@ Require Import Kildall.
 
 Definition valnum := positive.
 
-Inductive rhs : Set :=
+Inductive rhs : Type :=
   | Op: operation -> list valnum -> rhs
   | Load: memory_chunk -> addressing -> list valnum -> rhs.
 
@@ -85,7 +85,7 @@ Qed.
   we maintain the next unused value number, so as to easily generate
   fresh value numbers. *)
 
-Record numbering : Set := mknumbering {
+Record numbering : Type := mknumbering {
   num_next: valnum;
   num_eqs: list (valnum * rhs);
   num_reg: PTree.t valnum
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 35bf391..b48db2d 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -33,13 +33,13 @@ Require Import Switch.
   statements, functions and programs.  We first define the constants
   and operators that occur within expressions. *)
 
-Inductive constant : Set :=
+Inductive constant : Type :=
   | Ointconst: int -> constant     (**r integer constant *)
   | Ofloatconst: float -> constant (**r floating-point constant *)
   | Oaddrsymbol: ident -> int -> constant (**r address of the symbol plus the offset *)
   | Oaddrstack: int -> constant.   (**r stack pointer plus the given offset *)
 
-Inductive unary_operation : Set :=
+Inductive unary_operation : Type :=
   | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
@@ -55,7 +55,7 @@ Inductive unary_operation : Set :=
   | Ofloatofint: unary_operation           (**r float to signed integer *)
   | Ofloatofintu: unary_operation.         (**r float to unsigned integer *)
 
-Inductive binary_operation : Set :=
+Inductive binary_operation : Type :=
   | Oadd: binary_operation                 (**r integer addition *)
   | Osub: binary_operation                 (**r integer subtraction *)
   | Omul: binary_operation                 (**r integer multiplication *)
@@ -81,7 +81,7 @@ Inductive binary_operation : Set :=
   arithmetic operations, reading store locations, and conditional
   expressions (similar to [e1 ? e2 : e3] in C). *)
 
-Inductive expr : Set :=
+Inductive expr : Type :=
   | Evar : ident -> expr
   | Econst : constant -> expr
   | Eunop : unary_operation -> expr -> expr
@@ -97,7 +97,7 @@ Inductive expr : Set :=
 
 Definition label := ident.
 
-Inductive stmt : Set :=
+Inductive stmt : Type :=
   | Sskip: stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
@@ -120,7 +120,7 @@ Inductive stmt : Set :=
   automatically before the function returns.  Pointers into this block
   can be taken with the [Oaddrstack] operator. *)
 
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
   fn_sig: signature;
   fn_params: list ident;
   fn_vars: list ident;
@@ -172,7 +172,7 @@ Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
 
 (** Continuations *)
 
-Inductive cont: Set :=
+Inductive cont: Type :=
   | Kstop: cont                         (**r stop program execution *)
   | Kseq: stmt -> cont -> cont          (**r execute stmt, then cont *)
   | Kblock: cont -> cont                (**r exit a block, then do cont *)
@@ -181,7 +181,7 @@ Inductive cont: Set :=
 
 (** States *)
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State:                      (**r Execution within a function *)
       forall (f: function)              (**r currently executing function  *)
              (s: stmt)                  (**r statement under consideration *)
@@ -536,7 +536,7 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
     statements evaluate to``outcomes'' indicating how execution should
     proceed afterwards. *)
 
-Inductive outcome: Set :=
+Inductive outcome: Type :=
   | Out_normal: outcome                (**r continue in sequence *)
   | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
   | Out_return: option val -> outcome  (**r return immediately to caller *)
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index bfe92a4..1e798b5 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -40,7 +40,7 @@ Require Import Smallstep.
   boolean value only and not their exact value.
 *)
 
-Inductive expr : Set :=
+Inductive expr : Type :=
   | Evar : ident -> expr
   | Eop : operation -> exprlist -> expr
   | Eload : memory_chunk -> addressing -> exprlist -> expr
@@ -48,13 +48,13 @@ Inductive expr : Set :=
   | Elet : expr -> expr -> expr
   | Eletvar : nat -> expr
 
-with condexpr : Set :=
+with condexpr : Type :=
   | CEtrue: condexpr
   | CEfalse: condexpr
   | CEcond: condition -> exprlist -> condexpr
   | CEcondition : condexpr -> condexpr -> condexpr -> condexpr
 
-with exprlist : Set :=
+with exprlist : Type :=
   | Enil: exprlist
   | Econs: expr -> exprlist -> exprlist.
 
@@ -62,7 +62,7 @@ with exprlist : Set :=
   if/then/else conditional is a [condexpr], and the [Sstore] construct
   uses a machine-dependent addressing mode. *)
 
-Inductive stmt : Set :=
+Inductive stmt : Type :=
   | Sskip: stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
@@ -78,7 +78,7 @@ Inductive stmt : Set :=
   | Slabel: label -> stmt -> stmt
   | Sgoto: label -> stmt.
 
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
   fn_sig: signature;
   fn_params: list ident;
   fn_vars: list ident;
@@ -108,7 +108,7 @@ Definition letenv := list val.
 
 (** Continuations *)
 
-Inductive cont: Set :=
+Inductive cont: Type :=
   | Kstop: cont                         (**r stop program execution *)
   | Kseq: stmt -> cont -> cont          (**r execute stmt, then cont *)
   | Kblock: cont -> cont                (**r exit a block, then do cont *)
@@ -117,7 +117,7 @@ Inductive cont: Set :=
 
 (** States *)
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State:                              (**r execution within a function *)
       forall (f: function)              (**r currently executing function  *)
              (s: stmt)                  (**r statement under consideration *)
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 7204bc7..67824ae 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -93,7 +93,7 @@ Require Import InterfGraph.
 
 Definition add_interf_live
     (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
-  Regset.fold graph
+  Regset.fold 
     (fun r g => if filter r then add_interf r res g else g) live g.
 
 Definition add_interf_op
@@ -113,7 +113,7 @@ Definition add_interf_move
 Definition add_interf_destroyed
     (live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
   List.fold_left
-    (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g)
+    (fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g)
     destroyed g.
 
 Definition add_interfs_indirect_call
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index c86652a..92ac067 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -148,7 +148,7 @@ Qed.
 Lemma add_interf_destroyed_incl_aux_2:
   forall mr live g,
   graph_incl g
-    (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
+    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
 Proof.
   intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1.
 Qed.
@@ -219,7 +219,7 @@ Lemma add_interf_destroyed_correct_aux_2:
   forall mr live g r,
   Regset.In r live ->
   interfere_mreg r mr
-    (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
+    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
 Proof.
   intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1.
   apply Regset.elements_1. auto.
@@ -619,12 +619,12 @@ Lemma check_coloring_1_correct:
   coloring r1 <> coloring r2.
 Proof.
   unfold check_coloring_1. intros. 
-  assert (FSetInterface.compat_bool OrderedRegReg.eq
+  assert (compat_bool OrderedRegReg.eq
      (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2))
                   then false else true)).
   red. unfold OrderedRegReg.eq. unfold OrderedReg.eq.
   intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
-  generalize (SetRegReg.for_all_2 _ _ H1 H _ H0). 
+  generalize (SetRegReg.for_all_2 H1 H H0). 
   simpl. case (Loc.eq (coloring r1) (coloring r2)); intro.
   intro; discriminate. auto.
 Qed.
@@ -636,12 +636,12 @@ Lemma check_coloring_2_correct:
   coloring r1 <> R mr2.
 Proof.
   unfold check_coloring_2. intros. 
-  assert (FSetInterface.compat_bool OrderedRegMreg.eq
+  assert (compat_bool OrderedRegMreg.eq
      (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (R (snd r1r2))
                   then false else true)).
   red. unfold OrderedRegMreg.eq. unfold OrderedReg.eq.
   intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
-  generalize (SetRegMreg.for_all_2 _ _ H1 H _ H0). 
+  generalize (SetRegMreg.for_all_2 H1 H H0). 
   simpl. case (Loc.eq (coloring r1) (R mr2)); intro.
   intro; discriminate. auto.
 Qed.
@@ -920,12 +920,12 @@ Proof.
   intros. rewrite H2. unfold allregs. 
   elim (ordered_pair_charact x y); intro.
   apply alloc_of_coloring_correct_1. auto. 
-  change OrderedReg.t with reg. rewrite <- H6.
+  change positive with reg. rewrite <- H6.
   change (interfere x y g). unfold g. 
   apply interf_graph_correct_2; auto.
   apply sym_not_equal.
   apply alloc_of_coloring_correct_1. auto. 
-  change OrderedReg.t with reg. rewrite <- H6.
+  change positive with reg. rewrite <- H6.
   change (interfere x y g). unfold g. 
   apply interf_graph_correct_2; auto.
 Qed.
@@ -942,12 +942,12 @@ Proof.
   rewrite H4; unfold allregs.
   elim (ordered_pair_charact r1 r2); intro.
   apply alloc_of_coloring_correct_1. auto. 
-  change OrderedReg.t with reg. rewrite <- H5.
+  change positive with reg. rewrite <- H5.
   change (interfere r1 r2 g). unfold g.
   apply interf_graph_correct_3; auto.
   apply sym_not_equal.
   apply alloc_of_coloring_correct_1. auto. 
-  change OrderedReg.t with reg. rewrite <- H5.
+  change positive with reg. rewrite <- H5.
   change (interfere r1 r2 g). unfold g.
   apply interf_graph_correct_3; auto.
 Qed.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
index 433c074..8a9dda6 100644
--- a/backend/InterfGraph.v
+++ b/backend/InterfGraph.v
@@ -55,7 +55,7 @@ Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg).
 Module SetRegReg := FSetAVL.Make(OrderedRegReg).
 Module SetRegMreg := FSetAVL.Make(OrderedRegMreg).
 
-Record graph: Set := mkgraph {
+Record graph: Type := mkgraph {
   interf_reg_reg: SetRegReg.t;
   interf_reg_mreg: SetRegMreg.t;
   pref_reg_reg: SetRegReg.t;
@@ -160,7 +160,7 @@ Lemma add_interf_correct:
   interfere x y (add_interf x y g).
 Proof.
   intros. unfold interfere, add_interf; simpl.
-  apply SetRegReg.add_1. red. apply OrderedRegReg.eq_refl.
+  apply SetRegReg.add_1. auto. 
 Qed.
 
 Lemma add_interf_incl:
@@ -177,7 +177,7 @@ Lemma add_interf_mreg_correct:
   interfere_mreg x y (add_interf_mreg x y g).
 Proof.
   intros. unfold interfere_mreg, add_interf_mreg; simpl.
-  apply SetRegMreg.add_1. red. apply OrderedRegMreg.eq_refl.
+  apply SetRegMreg.add_1. auto. 
 Qed.
 
 Lemma add_interf_mreg_incl:
@@ -214,17 +214,17 @@ Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t :=
   Regset.add (fst r1m2) u.
 
 Definition all_interf_regs (g: graph) : Regset.t :=
-  SetRegReg.fold _ add_intf2
+  SetRegReg.fold add_intf2
     g.(interf_reg_reg)
-    (SetRegMreg.fold _ add_intf1
+    (SetRegMreg.fold add_intf1
       g.(interf_reg_mreg)
       Regset.empty).
 
 Lemma in_setregreg_fold:
   forall g r1 r2 u,
   SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
-  Regset.In r1 (SetRegReg.fold _ add_intf2 g u) /\
-  Regset.In r2 (SetRegReg.fold _ add_intf2 g u).
+  Regset.In r1 (SetRegReg.fold add_intf2 g u) /\
+  Regset.In r2 (SetRegReg.fold add_intf2 g u).
 Proof.
   set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u).
   assert (forall l r1 r2 u,
@@ -235,7 +235,7 @@ Proof.
   elim H; intro. inversion H0. auto.
   apply IHl. destruct a as [a1 a2].
   elim H; intro. inversion H0; subst. 
-  red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 r2.
+  red in H2. simpl in H2. destruct H2. subst r1 r2.
   right; unfold add_intf2', add_intf2; simpl; split.
   apply Regset.add_1. auto. 
   apply Regset.add_2. apply Regset.add_1. auto. 
@@ -250,7 +250,7 @@ Qed.
 Lemma in_setregreg_fold':
   forall g r u,
   Regset.In r u ->
-  Regset.In r (SetRegReg.fold _ add_intf2 g u).
+  Regset.In r (SetRegReg.fold add_intf2 g u).
 Proof.
   intros. exploit in_setregreg_fold. eauto. 
   intros [A B]. eauto.
@@ -259,7 +259,7 @@ Qed.
 Lemma in_setregmreg_fold:
   forall g r1 mr2 u,
   SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u ->
-  Regset.In r1 (SetRegMreg.fold _ add_intf1 g u).
+  Regset.In r1 (SetRegMreg.fold add_intf1 g u).
 Proof.
   set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u).
   assert (forall l r1 mr2 u,
@@ -269,7 +269,7 @@ Proof.
   elim H; intro. inversion H0. auto.
   apply IHl with mr2. destruct a as [a1 a2].
   elim H; intro. inversion H0; subst. 
-  red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 mr2.
+  red in H2. simpl in H2. destruct H2. subst r1 mr2.
   right; unfold add_intf1', add_intf1; simpl.
   apply Regset.add_1; auto.
   tauto.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index b4445ae..188a23f 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -108,7 +108,7 @@ End DATAFLOW_SOLVER.
 
 Module Type NODE_SET.
 
-  Variable t: Set.
+  Variable t: Type.
   Variable add: positive -> t -> t.
   Variable pick: t -> option (positive * t).
   Variable initial: positive -> t.
@@ -147,7 +147,7 @@ Variable entrypoints: list (positive * L.t).
 - A worklist of program points that remain to be considered.
 *)
 
-Record state : Set :=
+Record state : Type :=
   mkstate { st_in: PMap.t L.t; st_wrk: NS.t }.
 
 (** Kildall's algorithm, in pseudo-code, is as follows:
@@ -663,7 +663,7 @@ End Backward_Dataflow_Solver.
 
 Module Type ORDERED_TYPE_WITH_TOP.
 
-  Variable t: Set.
+  Variable t: Type.
   Variable ge: t -> t -> Prop.
   Variable top: t.
   Hypothesis top_ge: forall x, ge top x.
@@ -736,7 +736,7 @@ Definition result := PMap.t L.t.
 - A worklist of program points that remain to be considered.
 *)
 
-Record state : Set := mkstate
+Record state : Type := mkstate
   { st_in: result; st_wrk: list positive }.
 
 (** The ``extended basic block'' algorithm, in pseudo-code, is as follows:
@@ -1167,7 +1167,7 @@ Module NodeSetForward <: NODE_SET.
     rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. 
     elim (Plt_succ_inv _ _ H0); intro.
     right. apply H. auto.
-    left. red. red. auto.
+    left. auto.
   Qed.
 End NodeSetForward.
 
diff --git a/backend/LTL.v b/backend/LTL.v
index 0db5495..3a61e6d 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -34,7 +34,7 @@ Require Import Conventions.
 
 Definition node := positive.
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Lnop: node -> instruction
   | Lop: operation -> list loc -> loc -> node -> instruction
   | Lload: memory_chunk -> addressing -> list loc -> loc -> node -> instruction
@@ -44,9 +44,9 @@ Inductive instruction: Set :=
   | Lcond: condition -> list loc -> node -> node -> instruction
   | Lreturn: option loc -> instruction.
 
-Definition code: Set := PTree.t instruction.
+Definition code: Type := PTree.t instruction.
 
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
   fn_sig: signature;
   fn_params: list loc;
   fn_stacksize: Z;
@@ -103,7 +103,7 @@ Definition postcall_locs (ls: locset) : locset :=
 
 (** LTL execution states. *)
 
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
   | Stackframe:
       forall (res: loc)         (**r where to store the result *)
              (f: function)      (**r calling function *)
@@ -112,7 +112,7 @@ Inductive stackframe : Set :=
              (pc: node),        (**r program point in calling function *)
       stackframe.
 
-Inductive state : Set :=
+Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r function currently executing *)
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 4c87c0d..10b7d83 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -41,7 +41,7 @@ Definition label := positive.
   transfer control to the given code label.  Labels are explicitly
   inserted in the instruction list as pseudo-instructions [Llabel]. *)
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Lop: operation -> list loc -> loc -> instruction
   | Lload: memory_chunk -> addressing -> list loc -> loc -> instruction
   | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction
@@ -52,9 +52,9 @@ Inductive instruction: Set :=
   | Lcond: condition -> list loc -> label -> instruction
   | Lreturn: option loc -> instruction.
 
-Definition code: Set := list instruction.
+Definition code: Type := list instruction.
 
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
   fn_sig: signature;
   fn_params: list loc;
   fn_stacksize: Z;
@@ -109,7 +109,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
   code sequences [c] (suffixes of the code of the current function).
 *)
 
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
   | Stackframe:
       forall (res: loc)       (**r where to store the result *)
              (f: function)    (**r calling function *)
@@ -118,7 +118,7 @@ Inductive stackframe : Set :=
              (c: code),       (**r program point in calling function *)
       stackframe.
 
-Inductive state : Set :=
+Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r function currently executing *)
diff --git a/backend/Linear.v b/backend/Linear.v
index 34d6e5c..e025407 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -35,7 +35,7 @@ Require Import Conventions.
 
 Definition label := positive.
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Lgetstack: slot -> mreg -> instruction
   | Lsetstack: mreg -> slot -> instruction
   | Lop: operation -> list mreg -> mreg -> instruction
@@ -48,9 +48,9 @@ Inductive instruction: Set :=
   | Lcond: condition -> list mreg -> label -> instruction
   | Lreturn: instruction.
 
-Definition code: Set := list instruction.
+Definition code: Type := list instruction.
 
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
   fn_sig: signature;
   fn_stacksize: Z;
   fn_code: code
@@ -163,7 +163,7 @@ Definition return_regs (caller callee: locset) : locset :=
 
 (** Linear execution states. *)
 
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
   | Stackframe:
       forall (f: function)         (**r calling function *)
              (sp: val)             (**r stack pointer in calling function *)
@@ -171,7 +171,7 @@ Inductive stackframe: Set :=
              (c: code),            (**r program point in calling function *)
       stackframe.
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r function currently executing *)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index b385429..c24d370 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -193,7 +193,7 @@ Proof.
   generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
   exploit check_reachable_correct; eauto. intro.
   exploit nodeset_of_list_correct; eauto. intros [A [B C]].
-  rewrite B in H2. destruct H2. elim (Nodeset.empty_1 pc H2). auto.
+  rewrite B in H2. destruct H2. elim (Nodeset.empty_1 H2). auto.
 Qed.
 
 Lemma enumerate_norepet:
diff --git a/backend/Locations.v b/backend/Locations.v
index ca2f527..295df28 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -42,7 +42,7 @@ Require Export Machregs.
   cannot reside in hardware registers, as determined by the 
   calling conventions. *)
 
-Inductive slot: Set :=
+Inductive slot: Type :=
   | Local: Z -> typ -> slot
   | Incoming: Z -> typ -> slot
   | Outgoing: Z -> typ -> slot.
@@ -108,7 +108,7 @@ Qed.
 (** Locations are just the disjoint union of machine registers and
   activation record slots. *)
 
-Inductive loc : Set :=
+Inductive loc : Type :=
   | R: mreg -> loc
   | S: slot -> loc.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 3f25137..0bb2442 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -49,7 +49,7 @@ Require Import Locations.
 
 Definition label := positive.
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Mgetstack: int -> typ -> mreg -> instruction
   | Msetstack: mreg -> int -> typ -> instruction
   | Mgetparam: int -> typ -> mreg -> instruction
@@ -65,7 +65,7 @@ Inductive instruction: Set :=
 
 Definition code := list instruction.
 
-Record function: Set := mkfunction
+Record function: Type := mkfunction
   { fn_sig: signature;
     fn_code: code;
     fn_stacksize: Z;
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 25819f7..aa17cd4 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -51,7 +51,7 @@ Require Stacklayout.
     values.  Like location sets (see module [Locations]), overlap
     can occur. *)
 
-Definition frame : Set := typ -> Z -> val.
+Definition frame : Type := typ -> Z -> val.
 
 Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}.
 Proof. decide equality. Defined.
@@ -154,7 +154,7 @@ End FRAME_ACCESSES.
 
 (** Mach execution states. *)
 
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
   | Stackframe:
       forall (f: function)      (**r calling function *)
              (sp: val)          (**r stack pointer in calling function *)
@@ -162,7 +162,7 @@ Inductive stackframe: Set :=
              (fr: frame),       (**r frame state in calling function *)
       stackframe.
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r function currently executing *)
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 4417cc6..876f558 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -86,7 +86,7 @@ Definition extcall_arguments
 
 (** Mach execution states. *)
 
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
   | Stackframe:
       forall (f: block)       (**r pointer to calling function *)
              (sp: val)        (**r stack pointer in calling function *)
@@ -94,7 +94,7 @@ Inductive stackframe: Set :=
              (c: code),       (**r program point in calling function *)
       stackframe.
 
-Inductive state: Set :=
+Inductive state: Type :=
   | State:
       forall (stack: list stackframe)  (**r call stack *)
              (f: block)                (**r pointer to current function *)
diff --git a/backend/RTL.v b/backend/RTL.v
index 5fad2f2..344d271 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -44,7 +44,7 @@ Require Import Registers.
 
 Definition node := positive.
 
-Inductive instruction: Set :=
+Inductive instruction: Type :=
   | Inop: node -> instruction
       (** No operation -- just branch to the successor. *)
   | Iop: operation -> list reg -> reg -> node -> instruction
@@ -80,9 +80,9 @@ Inductive instruction: Set :=
           (it has no successor).  It returns the value of the given
           register, or [Vundef] if none is given. *)
 
-Definition code: Set := PTree.t instruction.
+Definition code: Type := PTree.t instruction.
 
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
   fn_sig: signature;
   fn_params: list reg;
   fn_stacksize: Z;
@@ -152,7 +152,7 @@ a function call in progress.
 [rs] is the state of registers in the calling function.
 *)
 
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
   | Stackframe:
       forall (res: reg)            (**r where to store the result *)
              (c: code)             (**r code of calling function *)
@@ -161,7 +161,7 @@ Inductive stackframe : Set :=
              (rs: regset),         (**r register state in calling function *)
       stackframe.
 
-Inductive state : Set :=
+Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (c: code)                (**r current code *)
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 709dc78..65e873e 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -36,7 +36,7 @@ Open Local Scope string_scope.
   The mapping for let-bound variables is initially empty and updated
   during translation of expressions, when crossing a [Elet] binding. *)
 
-Record mapping: Set := mkmapping {
+Record mapping: Type := mkmapping {
   map_vars: PTree.t reg;
   map_letvars: list reg
 }.
@@ -45,7 +45,7 @@ Record mapping: Set := mkmapping {
   current state of the control-flow graph for the function being translated,
   as well as sources of fresh RTL registers and fresh CFG nodes. *)
 
-Record state: Set := mkstate {
+Record state: Type := mkstate {
   st_nextreg: positive;
   st_nextnode: positive;
   st_code: code;
@@ -104,25 +104,25 @@ Qed.
   We now define this monadic encoding -- the ``state and error'' monad --
   as well as convenient syntax to express monadic computations. *)
 
-Inductive res (A: Set) (s: state): Set :=
+Inductive res (A: Type) (s: state): Type :=
   | Error: Errors.errmsg -> res A s
   | OK: A -> forall (s': state), state_incr s s' -> res A s.
 
 Implicit Arguments OK [A s].
 Implicit Arguments Error [A s].
 
-Definition mon (A: Set) : Set := forall (s: state), res A s.
+Definition mon (A: Type) : Type := forall (s: state), res A s.
 
-Definition ret (A: Set) (x: A) : mon A :=
+Definition ret (A: Type) (x: A) : mon A :=
   fun (s: state) => OK x s (state_incr_refl s).
 
 Implicit Arguments ret [A].
 
-Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
+Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
 
 Implicit Arguments error [A].
 
-Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
+Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B :=
   fun (s: state) =>
     match f s with
     | Error msg => Error msg
@@ -135,7 +135,7 @@ Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
 
 Implicit Arguments bind [A B].
 
-Definition bind2 (A B C: Set) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
   bind f (fun xy => g (fst xy) (snd xy)).
 
 Implicit Arguments bind2 [A B C].
@@ -145,7 +145,7 @@ Notation "'do' X <- A ; B" := (bind A (fun X => B))
 Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
    (at level 200, X ident, Y ident, A at level 100, B at level 200).
 
-Definition handle_error (A: Set) (f g: mon A) : mon A :=
+Definition handle_error (A: Type) (f g: mon A) : mon A :=
   fun (s: state) =>
     match f s with
     | OK a s' i => OK a s' i
@@ -498,7 +498,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
   [nlist] if it terminates by an [exit n] construct.  [rret] is the
   register where the return value of the function must be stored, if any. *)
 
-Definition labelmap : Set := PTree.t node.
+Definition labelmap : Type := PTree.t node.
 
 Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
                      (nexits: list node) (ngoto: labelmap) (nret: node) (rret: option reg)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index e6adeb0..8e61271 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -47,7 +47,7 @@ Require Import RTLgen.
 *)
 
 Remark bind_inversion:
-  forall (A B: Set) (f: mon A) (g: A -> mon B) 
+  forall (A B: Type) (f: mon A) (g: A -> mon B) 
          (y: B) (s1 s3: state) (i: state_incr s1 s3),
   bind f g s1 = OK y s3 i ->
   exists x, exists s2, exists i1, exists i2,
@@ -61,7 +61,7 @@ Proof.
 Qed.
 
 Remark bind2_inversion:
-  forall (A B C: Set) (f: mon (A*B)) (g: A -> B -> mon C)
+  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
          (z: C) (s1 s3: state) (i: state_incr s1 s3),
   bind2 f g s1 = OK z s3 i ->
   exists x, exists y, exists s2, exists i1, exists i2,
@@ -827,20 +827,6 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
 (** We now show that the translation functions in module [RTLgen]
   satisfy the specifications given above as inductive predicates. *)
 
-Scheme tr_expr_ind3 := Minimality for tr_expr Sort Prop
-  with tr_condition_ind3 := Minimality for tr_condition Sort Prop
-  with tr_exprlist_ind3 := Minimality for tr_exprlist Sort Prop.
-
-Definition tr_expr_condition_exprlist_ind3
-  (c: code)
-  (P : mapping -> list reg -> expr -> node -> node -> reg -> Prop)
-  (P0 : mapping -> list reg -> condexpr -> node -> node -> node -> Prop)
-  (P1 : mapping -> list reg -> exprlist -> node -> node -> list reg -> Prop) :=
-  fun a b c' d e f g h i j k l =>
-  conj (tr_expr_ind3 c P P0 P1 a b c' d e f g h i j k l)
-       (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l)
-             (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)).
-
 Lemma tr_move_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall ns rs nd rd,
@@ -850,69 +836,35 @@ Proof.
   induction 2; econstructor; eauto with rtlg.
 Qed.
 
-Lemma tr_expr_condition_exprlist_incr:
-  forall s1 s2, state_incr s1 s2 ->
-  (forall map pr a ns nd rd,
-   tr_expr s1.(st_code) map pr a ns nd rd ->
-   tr_expr s2.(st_code) map pr a ns nd rd)
-/\(forall map pr a ns ntrue nfalse,
-   tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
-   tr_condition s2.(st_code) map pr a ns ntrue nfalse)
-/\(forall map pr al ns nd rl,
-   tr_exprlist s1.(st_code) map pr al ns nd rl ->
-   tr_exprlist s2.(st_code) map pr al ns nd rl).
-Proof.
-  intros s1 s2 EXT. 
-  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
-  apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto.
-  eapply tr_move_incr; eauto.
-  eapply tr_move_incr; eauto.
-Qed.
-
 Lemma tr_expr_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr a ns nd rd,
   tr_expr s1.(st_code) map pr a ns nd rd ->
-  tr_expr s2.(st_code) map pr a ns nd rd.
-Proof.
-  intros.
-  exploit tr_expr_condition_exprlist_incr; eauto.
-  intros [A [B C]]. eauto.
-Qed.
-
-Lemma tr_condition_incr:
+  tr_expr s2.(st_code) map pr a ns nd rd
+with tr_condition_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr a ns ntrue nfalse,
   tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
-  tr_condition s2.(st_code) map pr a ns ntrue nfalse.
-Proof.
-  intros.
-  exploit tr_expr_condition_exprlist_incr; eauto. 
-  intros [A [B C]]. eauto.
-Qed.
-
-Lemma tr_exprlist_incr:
+  tr_condition s2.(st_code) map pr a ns ntrue nfalse
+with tr_exprlist_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr al ns nd rl,
   tr_exprlist s1.(st_code) map pr al ns nd rl ->
   tr_exprlist s2.(st_code) map pr al ns nd rl.
 Proof.
-  intros.
-  exploit tr_expr_condition_exprlist_incr; eauto.
-  intros [A [B C]]. eauto.
+  intros s1 s2 EXT. 
+  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+  induction 1; econstructor; eauto.
+  eapply tr_move_incr; eauto.
+  eapply tr_move_incr; eauto.
+  intros s1 s2 EXT. 
+  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+  induction 1; econstructor; eauto.
+  intros s1 s2 EXT. 
+  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+  induction 1; econstructor; eauto.
 Qed.
 
-Scheme expr_ind3 := Induction for expr Sort Prop
-  with condexpr_ind3 := Induction for condexpr Sort Prop
-  with exprlist_ind3 := Induction for exprlist Sort Prop.
-
-Definition expr_condexpr_exprlist_ind 
-    (P1: expr -> Prop) (P2: condexpr -> Prop) (P3: exprlist -> Prop) :=
-  fun a b c d e f g h i j k l =>
-  conj (expr_ind3 P1 P2 P3 a b c d e f g h i j k l)
-    (conj (condexpr_ind3 P1 P2 P3 a b c d e f g h i j k l)
-          (exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l)).
-
 Lemma add_move_charact:
   forall s ns rs nd rd s' i,
   add_move rs rd nd s = OK ns s' i -> 
@@ -923,30 +875,33 @@ Proof.
   constructor. eauto with rtlg.
 Qed.
 
-Lemma transl_expr_condexpr_list_charact:
-  (forall a map rd nd s ns s' pr INCR
+Lemma transl_expr_charact:
+  forall a map rd nd s ns s' pr INCR
      (TR: transl_expr map a rd nd s = OK ns s' INCR)
      (WF: map_valid map s)
      (OK: target_reg_ok map pr a rd)
      (VALID: regs_valid pr s)
      (VALID2: reg_valid rd s),
-   tr_expr s'.(st_code) map pr a ns nd rd)
-/\
-  (forall a map ntrue nfalse s ns s' pr INCR
+   tr_expr s'.(st_code) map pr a ns nd rd
+
+with transl_condexpr_charact:
+  forall a map ntrue nfalse s ns s' pr INCR
      (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
-     (WF: map_valid map s)
-     (VALID: regs_valid pr s),
-   tr_condition s'.(st_code) map pr a ns ntrue nfalse)
-/\
-  (forall al map rl nd s ns s' pr INCR
+     (VALID: regs_valid pr s)
+     (WF: map_valid map s),
+   tr_condition s'.(st_code) map pr a ns ntrue nfalse
+
+with transl_exprlist_charact:
+  forall al map rl nd s ns s' pr INCR
      (TR: transl_exprlist map al rl nd s = OK ns s' INCR)
      (WF: map_valid map s)
      (OK: target_regs_ok map pr al rl)
      (VALID1: regs_valid pr s)
      (VALID2: regs_valid rl s),
-   tr_exprlist s'.(st_code) map pr al ns nd rl).
+   tr_exprlist s'.(st_code) map pr al ns nd rl.
+
 Proof.
-  apply expr_condexpr_exprlist_ind; intros; try (monadInv TR).
+  induction a; intros; try (monadInv TR).
   (* Evar *)
   generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
   econstructor; eauto.
@@ -955,31 +910,31 @@ Proof.
   (* Eop *)
   inv OK.
   econstructor; eauto with rtlg.
-  eapply H; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   (* Eload *)
   inv OK.
   econstructor; eauto with rtlg.
-  eapply H; eauto with rtlg. 
+  eapply transl_exprlist_charact; eauto with rtlg. 
   (* Econdition *)
   inv OK.
   econstructor; eauto with rtlg.
-  eapply H; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_expr_incr with s1; auto. 
-  eapply H0; eauto with rtlg. constructor; auto. 
+  eapply transl_expr_charact; eauto with rtlg. constructor; auto.
   apply tr_expr_incr with s0; auto. 
-  eapply H1; eauto with rtlg. constructor; auto.
+  eapply transl_expr_charact; eauto with rtlg. constructor; auto.
   (* Elet *)
   inv OK.
   econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
-  eapply H; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg.
   apply tr_expr_incr with s1; auto.
-  eapply H0. eauto. 
+  eapply transl_expr_charact. eauto. 
   apply add_letvar_valid; eauto with rtlg. 
   constructor; auto. 
   red; unfold reg_in_map. simpl. intros [[id A] | [B | C]].
-  elim H1. left; exists id; auto.
+  elim H. left; exists id; auto.
   subst x. apply valid_fresh_absurd with rd s. auto. eauto with rtlg.
-  elim H1. right; auto.
+  elim H. right; auto.
   eauto with rtlg. eauto with rtlg.
   (* Eletvar *)
   generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0.
@@ -989,56 +944,41 @@ Proof.
   eapply add_move_charact; eauto.
   monadInv EQ1.
 
+(* Conditions *)
+  induction a; intros; try (monadInv TR).
+
   (* CEtrue *)
   constructor.
   (* CEfalse *)
   constructor.
   (* CEcond *)
   econstructor; eauto with rtlg.
-  eapply H; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   (* CEcondition *)
   econstructor.
-  eapply H; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_condition_incr with s1; auto.
-  eapply H0; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_condition_incr with s0; auto.
-  eapply H1; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
+
+(* Lists *)
+
+  induction al; intros; try (monadInv TR).
 
   (* Enil *)
   destruct rl; inv TR. constructor.
   (* Econs *)
   destruct rl; simpl in TR; monadInv TR. inv OK.
   econstructor.
-  eapply H; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg.
   generalize (VALID2 r (in_eq _ _)). eauto with rtlg.
   apply tr_exprlist_incr with s0; auto.
-  eapply H0; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   apply regs_valid_cons. apply VALID2. auto with coqlib. auto. 
   red; intros; apply VALID2; auto with coqlib.
 Qed.
 
-Lemma transl_expr_charact:
-  forall a map rd nd s ns s' INCR
-     (TR: transl_expr map a rd nd s = OK ns s' INCR)
-     (WF: map_valid map s)
-     (OK: target_reg_ok map nil a rd)
-     (VALID2: reg_valid rd s),
-   tr_expr s'.(st_code) map nil a ns nd rd.
-Proof.
-  destruct transl_expr_condexpr_list_charact as [A [B C]].
-  intros. eapply A; eauto with rtlg.
-Qed.
-
-Lemma transl_condexpr_charact:
-  forall a map ntrue nfalse s ns s' INCR
-     (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
-     (WF: map_valid map s),
-   tr_condition s'.(st_code) map nil a ns ntrue nfalse.
-Proof.
-  destruct transl_expr_condexpr_list_charact as [A [B C]].
-  intros. eapply B; eauto with rtlg.
-Qed.
-
 Lemma tr_store_var_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map rs id ns nd,
@@ -1076,7 +1016,7 @@ Lemma tr_stmt_incr:
   tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret.
 Proof.
   intros s1 s2 EXT.
-  destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]].
+  generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3.
   pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
   pose (STV := tr_store_var_incr s1 s2 EXT).
   pose (STOV := tr_store_optvar_incr s1 s2 EXT).
@@ -1148,19 +1088,17 @@ Proof.
   apply tr_store_var_incr with s1; auto with rtlg.
   eapply store_var_charact; eauto.
   (* Sstore *)
-  destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
   econstructor; eauto with rtlg.
-  eapply P3; eauto with rtlg. 
+  eapply transl_exprlist_charact; eauto with rtlg.
   apply tr_expr_incr with s3; eauto with rtlg.
-  eapply P1; eauto with rtlg. 
+  eapply transl_expr_charact; eauto with rtlg. 
   (* Scall *)
-  destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
   assert (state_incr s0 s3) by eauto with rtlg.
   assert (state_incr s3 s6) by eauto with rtlg.
   econstructor; eauto with rtlg.
-  eapply P1; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg.
   apply tr_exprlist_incr with s6. auto. 
-  eapply P3; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
   apply regs_valid_cons; eauto with rtlg.
   apply regs_valid_incr with s1; eauto with rtlg.
@@ -1169,13 +1107,12 @@ Proof.
   apply tr_store_optvar_incr with s4; eauto with rtlg.
   eapply store_optvar_charact; eauto with rtlg.
   (* Stailcall *)
-  destruct transl_expr_condexpr_list_charact as [A [B C]].
   assert (RV: regs_valid (x :: nil) s1).
     apply regs_valid_cons; eauto with rtlg. 
   econstructor; eauto with rtlg.
-  eapply A; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg.
   apply tr_exprlist_incr with s4; auto.
-  eapply C; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto. 
diff --git a/backend/Registers.v b/backend/Registers.v
index c3d04d6..fceb7c2 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -24,7 +24,7 @@ Require Import Ordered.
 Require Import FSets.
 Require FSetAVL.
 
-Definition reg: Set := positive.
+Definition reg: Type := positive.
 
 Module Reg.
 
@@ -41,14 +41,14 @@ Module Regmap := PMap.
 Set Implicit Arguments.
 
 Definition regmap_optget
-    (A: Set) (or: option reg) (dfl: A) (rs: Regmap.t A) : A :=
+    (A: Type) (or: option reg) (dfl: A) (rs: Regmap.t A) : A :=
   match or with
   | None => dfl
   | Some r => Regmap.get r rs
   end.
 
 Definition regmap_optset
-    (A: Set) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A :=
+    (A: Type) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A :=
   match or with
   | None => rs
   | Some r => Regmap.set r v rs
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 158af8f..182c322 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -34,7 +34,7 @@ Require Import Stacklayout.
 (** Computation the frame offset for the given component of the frame.
   The component is expressed by the following [frame_index] sum type. *)
 
-Inductive frame_index: Set :=
+Inductive frame_index: Type :=
   | FI_link: frame_index
   | FI_retaddr: frame_index
   | FI_local: Z -> typ -> frame_index
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index a7560d0..d5819f7 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -955,7 +955,7 @@ Proof.
   exists ls'; exists rs'. split. assumption.
   split. intros. elim H2; intros. 
   subst r. apply (agree_unused_reg _ _ _ _ _ D).
-  rewrite <- number_within_bounds. auto. omega. auto.
+  rewrite <- number_within_bounds. auto. auto. auto.
   split. intros. simpl in H2. apply C. tauto.
   assumption.
 Qed.
@@ -1051,7 +1051,7 @@ End FRAME_PROPERTIES.
 Section LABELS.
 
 Remark find_label_fold_right:
-  forall (A: Set) (fn: A -> Mach.code -> Mach.code) lbl,
+  forall (A: Type) (fn: A -> Mach.code -> Mach.code) lbl,
   (forall x k, Mach.find_label lbl (fn x k) = Mach.find_label lbl k) ->  forall (args: list A) k,
   Mach.find_label lbl (List.fold_right fn k args) = Mach.find_label lbl k.
 Proof.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index b88dd50..1bafc35 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -51,7 +51,7 @@ Variable tf: Mach.function.
 Hypothesis TRANSF_F: transf_function f = OK tf.
 
 Lemma wt_fold_right:
-  forall (A: Set) (f: A -> code -> code) (k: code) (l: list A),
+  forall (A: Type) (f: A -> code -> code) (k: code) (l: list A),
   (forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) ->
   wt_instrs k ->
   wt_instrs (List.fold_right f k l).
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 8e97e1a..791db37 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -574,8 +574,8 @@ Proof.
   exploit loadv_lessdef; eauto. 
   intros [v' [LOAD' VLD]].
   left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split.
-  eapply exec_Iload; eauto.  rewrite <- ADDR'.
-  apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload with (a := a'). eauto.  rewrite <- ADDR'.
+  apply eval_addressing_preserved. exact symbols_preserved. eauto.
   econstructor; eauto. apply regset_set; auto.
 
 (* store *)
@@ -586,8 +586,8 @@ Proof.
   exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD.  
   intros [m'1 [STORE' MLD']].
   left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split.
-  eapply exec_Istore; eauto.  rewrite <- ADDR'.
-  apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Istore with (a := a'). eauto.  rewrite <- ADDR'.
+  apply eval_addressing_preserved. exact symbols_preserved. eauto.
   destruct a; simpl in H1; try discriminate.
   econstructor; eauto.
   eapply match_stacksize_store; eauto. 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 49bf894..08f5f6c 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -268,16 +268,18 @@ Proof.
   (* Lload *)
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
   left; econstructor; split.
-  eapply exec_Lload; eauto.
+  eapply exec_Lload with (a := a). 
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto.
   econstructor; eauto.
   (* Lstore *)
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
   left; econstructor; split.
-  eapply exec_Lstore; eauto.
+  eapply exec_Lstore with (a := a).
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.  
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto.
   econstructor; eauto.
   (* Lcall *)
   left; econstructor; split.