Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 755 insertions, 1016 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index a3afae20..23faf785 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -3,6 +3,7 @@
 Require Import FSets.
 Require FSetAVL.
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Ordered.
 Require Import AST.
@@ -11,7 +12,9 @@ Require Mem.
 Require Import Csharpminor.
 Require Import Op.
 Require Import Cminor.
-Require Cmconstr.
+
+Open Local Scope string_scope.
+Open Local Scope error_monad_scope.
 
 (** The main task in translating Csharpminor to Cminor is to explicitly
   stack-allocate local variables whose address is taken: these local
@@ -35,57 +38,12 @@ Require Cmconstr.
   the ``normalize at assignment-time'' semantics of Csharpminor.
 *)
 
-(** Translation of operators. *)
+(** Translation of constants. *)
 
-Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr :=
-  match el with
-  | Enil =>
-      match op with
-      | Csharpminor.Ointconst n => Some(Eop (Ointconst n) Enil)
-      | Csharpminor.Ofloatconst n => Some(Eop (Ofloatconst n) Enil)
-      | _ => None
-      end
-  | Econs e1 Enil =>
-      match op with
-      | Csharpminor.Ocast8unsigned => Some(Cmconstr.cast8unsigned e1)
-      | Csharpminor.Ocast8signed => Some(Cmconstr.cast8signed e1)
-      | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1)
-      | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1)
-      | Csharpminor.Onotint => Some(Cmconstr.notint e1)
-      | Csharpminor.Onotbool => Some(Cmconstr.notbool e1)
-      | Csharpminor.Onegf => Some(Cmconstr.negfloat e1)
-      | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1)
-      | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1)
-      | Csharpminor.Ointoffloat => Some(Cmconstr.intoffloat e1)
-      | Csharpminor.Ofloatofint => Some(Cmconstr.floatofint e1)
-      | Csharpminor.Ofloatofintu => Some(Cmconstr.floatofintu e1)
-      | _ => None
-      end
-  | Econs e1 (Econs e2 Enil) =>
-      match op with
-      | Csharpminor.Oadd => Some(Cmconstr.add e1 e2)
-      | Csharpminor.Osub => Some(Cmconstr.sub e1 e2)
-      | Csharpminor.Omul => Some(Cmconstr.mul e1 e2)
-      | Csharpminor.Odiv => Some(Cmconstr.divs e1 e2)
-      | Csharpminor.Odivu => Some(Cmconstr.divu e1 e2)
-      | Csharpminor.Omod => Some(Cmconstr.mods e1 e2)
-      | Csharpminor.Omodu => Some(Cmconstr.modu e1 e2)
-      | Csharpminor.Oand => Some(Cmconstr.and e1 e2)
-      | Csharpminor.Oor => Some(Cmconstr.or e1 e2)
-      | Csharpminor.Oxor => Some(Cmconstr.xor e1 e2)
-      | Csharpminor.Oshl => Some(Cmconstr.shl e1 e2)
-      | Csharpminor.Oshr => Some(Cmconstr.shr e1 e2)
-      | Csharpminor.Oshru => Some(Cmconstr.shru e1 e2)
-      | Csharpminor.Oaddf => Some(Cmconstr.addf e1 e2)
-      | Csharpminor.Osubf => Some(Cmconstr.subf e1 e2)
-      | Csharpminor.Omulf => Some(Cmconstr.mulf e1 e2)
-      | Csharpminor.Odivf => Some(Cmconstr.divf e1 e2)
-      | Csharpminor.Ocmp c => Some(Cmconstr.cmp c e1 e2)
-      | Csharpminor.Ocmpu c => Some(Cmconstr.cmpu c e1 e2)
-      | Csharpminor.Ocmpf c => Some(Cmconstr.cmpf c e1 e2)
-      | _ => None
-      end
-  | _ => None
+Definition transl_constant (cst: Csharpminor.constant): constant :=
+  match cst with
+  | Csharpminor.Ointconst n => Ointconst n
+  | Csharpminor.Ofloatconst n => Ofloatconst n
   end.
 
 (** [make_cast chunk e] returns a Cminor expression that normalizes
@@ -95,45 +53,38 @@ Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr :=
 
 Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
   match chunk with
-  | Mint8signed => Cmconstr.cast8signed e
-  | Mint8unsigned => Cmconstr.cast8unsigned e
-  | Mint16signed => Cmconstr.cast16signed e
-  | Mint16unsigned => Cmconstr.cast16unsigned e
+  | Mint8signed => Eunop Ocast8signed e
+  | Mint8unsigned => Eunop Ocast8unsigned e
+  | Mint16signed => Eunop Ocast16signed e
+  | Mint16unsigned => Eunop Ocast16unsigned e
   | Mint32 => e
-  | Mfloat32 => Cmconstr.singleoffloat e
+  | Mfloat32 => Eunop Osingleoffloat e
   | Mfloat64 => e
   end.
 
-Definition make_load (chunk: memory_chunk) (e: expr): expr :=
-  Cmconstr.load chunk e.
-
 Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
   match e with
-  | Eop op (Econs e1 Enil) =>
-      match op with
-      | Ocast8signed =>
-          match chunk with Mint8signed => e1 | _ => e end
-      | Ocast8unsigned =>
-          match chunk with Mint8unsigned => e1 | _ => e end
-      | Ocast16signed =>
-          match chunk with Mint16signed => e1 | _ => e end
-      | Ocast16unsigned =>
-          match chunk with Mint16unsigned => e1 | _ => e end
-      | Osingleoffloat =>
-          match chunk with Mfloat32 => e1 | _ => e end
-      | _ => e
-      end
+  | Eunop Ocast8signed e1 =>
+      match chunk with Mint8signed => e1 | _ => e end
+  | Eunop Ocast8unsigned e1 =>
+      match chunk with Mint8unsigned => e1 | _ => e end
+  | Eunop Ocast16signed e1 =>
+      match chunk with Mint16signed => e1 | _ => e end
+  | Eunop Ocast16unsigned e1 =>
+      match chunk with Mint16unsigned => e1 | _ => e end
+  | Eunop Osingleoffloat e1 =>
+      match chunk with Mfloat32 => e1 | _ => e end
   | _ => e
   end.
 
 Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt :=
-  Sexpr(Cmconstr.store chunk e1 (store_arg chunk e2)).
+  Sexpr (Estore chunk e1 (store_arg chunk e2)).
 
 Definition make_stackaddr (ofs: Z): expr :=
-  Eop (Oaddrstack (Int.repr ofs)) Enil.
+  Econst (Oaddrstack (Int.repr ofs)).
 
 Definition make_globaladdr (id: ident): expr :=
-  Eop (Oaddrsymbol id Int.zero) Enil.
+  Econst (Oaddrsymbol id Int.zero).
 
 (** Compile-time information attached to each Csharpminor
   variable: global variables, local variables, function parameters.
@@ -156,134 +107,127 @@ Definition compilenv := PMap.t var_info.
 (** Generation of Cminor code corresponding to accesses to Csharpminor 
   local variables: reads, assignments, and taking the address of. *)
 
-Definition var_get (cenv: compilenv) (id: ident): option expr :=
+Definition var_get (cenv: compilenv) (id: ident): res expr :=
   match PMap.get id cenv with
   | Var_local chunk =>
-      Some(Evar id)
+      OK(Evar id)
   | Var_stack_scalar chunk ofs =>
-      Some(make_load chunk (make_stackaddr ofs))
+      OK(Eload chunk (make_stackaddr ofs))
   | Var_global_scalar chunk =>
-      Some(make_load chunk (make_globaladdr id))
+      OK(Eload chunk (make_globaladdr id))
   | _ =>
-      None
+      Error(msg "Cminorgen.var_get")
   end.
 
-Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt :=
+Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): res stmt :=
   match PMap.get id cenv with
   | Var_local chunk =>
-      Some(Sassign id (make_cast chunk rhs))
+      OK(Sassign id (make_cast chunk rhs))
   | Var_stack_scalar chunk ofs =>
-      Some(make_store chunk (make_stackaddr ofs) rhs)
+      OK(make_store chunk (make_stackaddr ofs) rhs)
   | Var_global_scalar chunk =>
-      Some(make_store chunk (make_globaladdr id) rhs)
+      OK(make_store chunk (make_globaladdr id) rhs)
   | _ =>
-      None
+      Error(msg "Cminorgen.var_set")
   end.
 
-Definition var_addr (cenv: compilenv) (id: ident): option expr :=
+Definition var_addr (cenv: compilenv) (id: ident): res expr :=
   match PMap.get id cenv with
-  | Var_local chunk => None
-  | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs)
-  | Var_stack_array ofs => Some (make_stackaddr ofs)
-  | _ => Some (make_globaladdr id)
-  end.
-
-(** The translation from Csharpminor to Cminor can fail, which we
-  encode by returning option types ([None] denotes error).
-  Propagation of errors is done in monadic style, using the following
-  [bind] monadic composition operator, and a [do] notation inspired
-  by Haskell's. *)
-
-Definition bind (A B: Set) (a: option A) (b: A -> option B): option B :=
-  match a with
-  | None => None
-  | Some x => b x
+  | Var_local chunk => Error(msg "Cminorgen.var_addr")
+  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs)
+  | Var_stack_array ofs => OK (make_stackaddr ofs)
+  | _ => OK (make_globaladdr id)
   end.
 
-Notation "'do' X <- A ; B" := (bind _ _ A (fun X => B))
-  (at level 200, X ident, A at level 100, B at level 200).
-
 (** Translation of expressions.  All the hard work is done by the
   [make_*] and [var_*] functions defined above. *)
 
 Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
-                     {struct e}: option expr :=
+                     {struct e}: res expr :=
   match e with
   | Csharpminor.Evar id => var_get cenv id
   | Csharpminor.Eaddrof id => var_addr cenv id
-  | Csharpminor.Eop op el =>
-      do tel <- transl_exprlist cenv el; make_op op tel
+  | Csharpminor.Econst cst =>
+      OK (Econst (transl_constant cst))
+  | Csharpminor.Eunop op e1 =>
+      do te1 <- transl_expr cenv e1;
+      OK (Eunop op te1)
+  | Csharpminor.Ebinop op e1 e2 =>
+      do te1 <- transl_expr cenv e1;
+      do te2 <- transl_expr cenv e2;
+      OK (Ebinop op te1 te2)
   | Csharpminor.Eload chunk e =>
-      do te <- transl_expr cenv e; Some (make_load chunk te)
+      do te <- transl_expr cenv e;
+      OK (Eload chunk te)
   | Csharpminor.Ecall sig e el =>
       do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
-      Some (Ecall sig te tel)
+      OK (Ecall sig te tel)
   | Csharpminor.Econdition e1 e2 e3 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
       do te3 <- transl_expr cenv e3;
-      Some (Cmconstr.conditionalexpr te1 te2 te3)
+      OK (Econdition te1 te2 te3)
   | Csharpminor.Elet e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
-      Some (Elet te1 te2)
+      OK (Elet te1 te2)
   | Csharpminor.Eletvar n =>
-      Some (Eletvar n)
+      OK (Eletvar n)
   | Csharpminor.Ealloc e =>
       do te <- transl_expr cenv e;
-      Some (Ealloc te)
+      OK (Ealloc te)
   end
 
 with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist)
-                     {struct el}: option exprlist :=
+                     {struct el}: res exprlist :=
   match el with
   | Csharpminor.Enil =>
-      Some Enil
+      OK Enil
   | Csharpminor.Econs e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_exprlist cenv e2;
-      Some (Econs te1 te2)
+      OK (Econs te1 te2)
   end.
 
 (** Translation of statements.  Entirely straightforward. *)
 
 Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt)
-                     {struct s}: option stmt :=
+                     {struct s}: res stmt :=
   match s with
   | Csharpminor.Sskip =>
-      Some Sskip
+      OK Sskip
   | Csharpminor.Sexpr e =>
-      do te <- transl_expr cenv e; Some(Sexpr te)
+      do te <- transl_expr cenv e; OK(Sexpr te)
   | Csharpminor.Sassign id e =>
       do te <- transl_expr cenv e; var_set cenv id te
   | Csharpminor.Sstore chunk e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
-      Some (make_store chunk te1 te2)
+      OK (make_store chunk te1 te2)
   | Csharpminor.Sseq s1 s2 =>
       do ts1 <- transl_stmt cenv s1;
       do ts2 <- transl_stmt cenv s2;
-      Some (Sseq ts1 ts2)
+      OK (Sseq ts1 ts2)
   | Csharpminor.Sifthenelse e s1 s2 =>
       do te <- transl_expr cenv e;
       do ts1 <- transl_stmt cenv s1;
       do ts2 <- transl_stmt cenv s2;
-      Some (Cmconstr.ifthenelse te ts1 ts2)
+      OK (Sifthenelse te ts1 ts2)
   | Csharpminor.Sloop s =>
       do ts <- transl_stmt cenv s;
-      Some (Sloop ts)
+      OK (Sloop ts)
   | Csharpminor.Sblock s =>
       do ts <- transl_stmt cenv s;
-      Some (Sblock ts)
+      OK (Sblock ts)
   | Csharpminor.Sexit n =>
-      Some (Sexit n)
+      OK (Sexit n)
   | Csharpminor.Sswitch e cases default =>
-      do te <- transl_expr cenv e; Some(Sswitch te cases default)
+      do te <- transl_expr cenv e; OK(Sswitch te cases default)
   | Csharpminor.Sreturn None =>
-      Some (Sreturn None)
+      OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do te <- transl_expr cenv e; Some (Sreturn (Some te))
+      do te <- transl_expr cenv e; OK (Sreturn (Some te))
   end.
 
 (** Computation of the set of variables whose address is taken in
@@ -295,7 +239,10 @@ Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t :=
   match e with
   | Csharpminor.Evar id => Identset.empty
   | Csharpminor.Eaddrof id => Identset.add id Identset.empty
-  | Csharpminor.Eop op el => addr_taken_exprlist el
+  | Csharpminor.Econst cst => Identset.empty
+  | Csharpminor.Eunop op e1 => addr_taken_expr e1
+  | Csharpminor.Ebinop op e1 e2 =>
+      Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
   | Csharpminor.Eload chunk e => addr_taken_expr e
   | Csharpminor.Ecall sig e el =>
       Identset.union (addr_taken_expr e) (addr_taken_exprlist el)
@@ -416,23 +363,23 @@ Fixpoint store_parameters
   overflow machine arithmetic and lead to incorrect code. *)
 
 Definition transl_function
-         (gce: compilenv) (f: Csharpminor.function): option function :=
+         (gce: compilenv) (f: Csharpminor.function): res function :=
   let (cenv, stacksize) := build_compilenv gce f in
   if zle stacksize Int.max_signed then
     do tbody <- transl_stmt cenv f.(Csharpminor.fn_body);
-       Some (mkfunction
+       OK (mkfunction
               (Csharpminor.fn_sig f)
               (Csharpminor.fn_params_names f)
               (Csharpminor.fn_vars_names f)
               stacksize
               (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody))
-  else None.
+  else Error(msg "Cminorgen: too many local variables, stack size exceeded").
 
-Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef :=
+Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): res fundef :=
   transf_partial_fundef (transl_function gce) f.
 
-Definition transl_globvar (vk: var_kind) := Some tt.
+Definition transl_globvar (vk: var_kind) := OK tt.
 
-Definition transl_program (p: Csharpminor.program) : option program :=
+Definition transl_program (p: Csharpminor.program) : res program :=
   let gce := build_global_compilenv p in
   transform_partial_program2 (transl_fundef gce) transl_globvar p.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ad31ff19..5bcb8801 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -2,6 +2,7 @@
 
 Require Import FSets.
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
@@ -11,68 +12,49 @@ Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Csharpminor.
-Require Import Op.
 Require Import Cminor.
-Require Cmconstr.
 Require Import Cminorgen.
-Require Import Cmconstrproof.
+
+Open Local Scope error_monad_scope.
 
 Section TRANSLATION.
 
 Variable prog: Csharpminor.program.
 Variable tprog: program.
-Hypothesis TRANSL: transl_program prog = Some tprog.
+Hypothesis TRANSL: transl_program prog = OK tprog.
 Let ge : Csharpminor.genv := Genv.globalenv prog.
 Let tge: genv := Genv.globalenv tprog.
 Let gce : compilenv := build_global_compilenv prog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intro. unfold ge, tge. 
-  apply Genv.find_symbol_transf_partial2 with (transl_fundef gce) transl_globvar.
-  exact TRANSL.
-Qed.
+Proof (Genv.find_symbol_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Csharpminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = Some tf.
-Proof.
-  intros. 
-  generalize 
-   (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H).
-  case (transl_fundef gce f).
-  intros tf [A B]. exists tf. tauto.
-  intros [A B]. elim B. reflexivity.
-Qed.
+  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).
+
 
 Lemma functions_translated:
   forall (v: val) (f: Csharpminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
-  Genv.find_funct tge v = Some tf /\ transl_fundef gce f = Some tf.
-Proof.
-  intros. 
-  generalize 
-   (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H).
-  case (transl_fundef gce f).
-  intros tf [A B]. exists tf. tauto.
-  intros [A B]. elim B. reflexivity.
-Qed.
+  Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf.
+Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).
 
 Lemma sig_preserved:
   forall f tf,
-  transl_fundef gce f = Some tf -> 
+  transl_fundef gce f = OK tf -> 
   Cminor.funsig tf = Csharpminor.funsig f.
 Proof.
   intros until tf; destruct f; simpl.
   unfold transl_function. destruct (build_compilenv gce f).
-  case (zle z Int.max_signed); try congruence.
-  intro. case (transl_stmt c (Csharpminor.fn_body f)); simpl; try congruence.
-  intros. inversion H. reflexivity.
-  intro. inversion H; reflexivity.
+  case (zle z Int.max_signed); simpl; try congruence.
+  intros. monadInv H. monadInv EQ. reflexivity.
+  intro. inv H. reflexivity.
 Qed.
 
 Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop :=
@@ -510,15 +492,12 @@ Lemma load_from_alloc_is_undef:
   alloc m1 0 (size_chunk chunk) = (m2, b) ->
   load chunk m2 b 0 = Some Vundef.
 Proof.
-  intros. 
-  assert (valid_block m2 b). eapply valid_new_block; eauto.
-  assert (low_bound m2 b <= 0). 
-    generalize (low_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega.
-  assert (0 + size_chunk chunk <= high_bound m2 b).
-    generalize (high_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega.
-  elim (load_in_bounds _ _ _ _ H0 H1 H2). intros v LOAD.
-  assert (v = Vundef). eapply load_alloc_same; eauto.
-  congruence.
+  intros.
+  assert (exists v, load chunk m2 b 0 = Some v).
+    apply valid_access_load.
+    eapply valid_access_alloc_same; eauto; omega.
+  destruct H0 as [v LOAD]. rewrite LOAD. decEq. 
+  eapply load_alloc_same; eauto.
 Qed.
 
 Lemma match_env_alloc_same:
@@ -577,14 +556,20 @@ Proof.
       contradiction.
     (* other vars *)
     generalize (me_vars0 id0); intros.
-    inversion H6; econstructor; eauto.
-    unfold e2; rewrite PTree.gso; auto. 
-    unfold f2, extend_inject, eq_block; rewrite zeq_false; auto.
-    generalize (me_bounded0 _ _ _ H8). unfold block in *; omega.
-    unfold e2; rewrite PTree.gso; eauto. 
-    unfold e2; rewrite PTree.gso; eauto. 
-    unfold e2; rewrite PTree.gso; eauto. 
-    unfold e2; rewrite PTree.gso; eauto. 
+    inversion H6.
+    eapply match_var_local with (v := v); eauto.
+      unfold e2; rewrite PTree.gso; eauto.
+      eapply load_alloc_other; eauto. 
+      unfold f2, extend_inject, eq_block; rewrite zeq_false; auto.
+      generalize (me_bounded0 _ _ _ H8). unfold block in *; omega.
+    econstructor; eauto.
+      unfold e2; rewrite PTree.gso; eauto.
+    econstructor; eauto. 
+      unfold e2; rewrite PTree.gso; eauto. 
+    econstructor; eauto.
+      unfold e2; rewrite PTree.gso; eauto.
+    econstructor; eauto. 
+      unfold e2; rewrite PTree.gso; eauto. 
   (* lo <= hi *)
   unfold block in *; omega.
   (* me_bounded *)
@@ -629,9 +614,15 @@ Proof.
   inversion H2. constructor; auto.
   (* me_vars *)
   intros. generalize (me_vars0 id); intro. 
-  inversion H5; econstructor; eauto.
-  unfold f2, extend_inject, eq_block. rewrite zeq_false. auto.
-  generalize (me_bounded0 _ _ _ H7). unfold block in *; omega.
+  inversion H5.
+  eapply match_var_local with (v := v); eauto.
+    eapply load_alloc_other; eauto.
+    unfold f2, extend_inject, eq_block. rewrite zeq_false. auto.
+    generalize (me_bounded0 _ _ _ H7). unfold block in *; omega.
+  econstructor; eauto.
+  econstructor; eauto.
+  econstructor; eauto.
+  econstructor; eauto.
   (* me_bounded *)
   intros until delta. unfold f2, extend_inject, eq_block.
   case (zeq b0 b); intros. rewrite H5 in H0. omegaContradiction.
@@ -726,9 +717,10 @@ Proof.
   (* me_vars *)
   intros. generalize (me_vars0 id); intro. inversion H5.
     (* var_local *)
-    econstructor; eauto. 
+    eapply match_var_local with (v := v); eauto.
+    eapply load_alloc_other; eauto. 
     generalize (me_bounded0 _ _ _ H7). intro. 
-    unfold f2, extend_inject. case (eq_block b0 b); intro. 
+    unfold f2, extend_inject. case (zeq b0 b); intro. 
     subst b0. rewrite BEQ in H12. omegaContradiction. 
     auto.
     (* var_stack_scalar *)
@@ -740,12 +732,12 @@ Proof.
     (* var_global_array *)
     econstructor; eauto.
   (* me_bounded *)
-  intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intro.
+  intros until delta. unfold f2, extend_inject. case (zeq b0 b); intro.
   intro. injection H5; clear H5; intros. 
   rewrite H6 in TBEQ. rewrite TBEQ in H3. omegaContradiction.
   eauto.
   (* me_inj *)
-  intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intros.
+  intros until delta. unfold f2, extend_inject. case (zeq b0 b); intros.
   injection H5; clear H5; intros; subst b0 tb0 delta.
   rewrite BEQ in H6. omegaContradiction. 
   eauto.
@@ -804,16 +796,7 @@ Qed.
 
 (** * Correctness of Cminor construction functions *)
 
-Hint Resolve eval_negint eval_negfloat eval_absfloat eval_intoffloat
-  eval_floatofint eval_floatofintu eval_notint eval_notbool
-  eval_cast8signed eval_cast8unsigned eval_cast16signed
-  eval_cast16unsigned eval_singleoffloat eval_add eval_add_ptr
-  eval_add_ptr_2 eval_sub eval_sub_ptr_int eval_sub_ptr_ptr
-  eval_mul eval_divs eval_mods eval_divu eval_modu
-  eval_and eval_or eval_xor eval_shl eval_shr eval_shru 
-  eval_addf eval_subf eval_mulf eval_divf
-  eval_cmp eval_cmp_null_r eval_cmp_null_l eval_cmp_ptr
-  eval_cmpu eval_cmpf: evalexpr.
+Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr.
 
 Remark val_inject_val_of_bool:
   forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
@@ -821,151 +804,146 @@ Proof.
   intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor.
 Qed.
 
+Remark val_inject_bool_of_val:
+  forall f v b tv,
+  val_inject f v tv -> Val.bool_of_val v b -> Val.bool_of_val tv b.
+Proof.
+  intros. inv H; inv H0; constructor; auto.
+Qed.
+
+Remark val_inject_eval_compare_null:
+  forall f c i v,  
+  eval_compare_null c i = Some v ->
+  val_inject f v v.
+Proof.
+  unfold eval_compare_null; intros.
+  destruct (Int.eq i Int.zero). 
+  destruct c; inv H; unfold Vfalse, Vtrue; constructor.
+  discriminate.
+Qed.
+
 Ltac TrivialOp :=
   match goal with
-  | [ |- exists x, _ /\ val_inject _ (Vint ?x) _ ] =>
+  | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] =>
       exists (Vint x); split;
       [eauto with evalexpr | constructor]
-  | [ |- exists x, _ /\ val_inject _ (Vfloat ?x) _ ] =>
+  | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] =>
       exists (Vfloat x); split;
       [eauto with evalexpr | constructor]
-  | [ |- exists x, _ /\ val_inject _ (Val.of_bool ?x) _ ] =>
+  | [ |- exists y, _ /\ val_inject _ (Val.of_bool ?x) _ ] =>
       exists (Val.of_bool x); split;
       [eauto with evalexpr | apply val_inject_val_of_bool]
+  | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] =>
+      exists x; split; [auto | econstructor; eauto]
   | _ => idtac
   end.
 
-Remark eval_compare_null_inv:
-  forall c i v,
-  Csharpminor.eval_compare_null c i = Some v ->
-  i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue).
+(** Correctness of [transl_constant]. *)
+
+Lemma transl_constant_correct:
+  forall f sp cst v,
+  Csharpminor.eval_constant cst = Some v ->
+  exists tv,
+     eval_constant tge sp (transl_constant cst) = Some tv
+  /\ val_inject f v tv.
 Proof.
-  intros until v. unfold Csharpminor.eval_compare_null.
-  predSpec Int.eq Int.eq_spec i Int.zero.
-  case c; intro EQ; simplify_eq EQ; intro; subst v; tauto.
-  congruence.
+  destruct cst; simpl; intros; inv H; TrivialOp.
 Qed.
 
-(** Correctness of [make_op].  The generated Cminor code evaluates
-  to a value that matches the result value of the Csharpminor operation,
-  provided arguments match pairwise ([val_list_inject f] hypothesis). *)
+(** Compatibility of [eval_unop] with respect to [val_inject]. *)
 
-Lemma make_op_correct:
-  forall al a op vl m2 v sp le te tm1 t tm2 tvl f,
-  make_op op al = Some a ->
-  Csharpminor.eval_operation op vl m2 = Some v ->
-  eval_exprlist tge (Vptr sp Int.zero) le te tm1 al t tm2 tvl ->
-  val_list_inject f vl tvl ->
-  mem_inject f m2 tm2 ->
+Lemma eval_unop_compat:
+  forall f op v1 tv1 v,
+  eval_unop op v1 = Some v ->
+  val_inject f v1 tv1 ->
   exists tv,
-     eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv
+     eval_unop op tv1 = Some tv
   /\ val_inject f v tv.
 Proof.
-  intros. 
-  destruct al as [ | a1 al];
-  [idtac | destruct al as [ | a2 al];
-  [idtac | destruct al as [ | a3 al]]];
-  simpl in H; try discriminate.
-  (* Constant operators *)
-  inversion H1. subst sp0 le0 e m tm1 tvl.
-  inversion H2. subst vl.
-  destruct op; simplify_eq H; intro; subst a;
-  simpl in H0; injection H0; intro; subst v.
-  (* intconst *)
-  TrivialOp. econstructor. constructor. reflexivity. 
-  (* floatconst *)
-  TrivialOp. econstructor. constructor. reflexivity.
-  (* Unary operators *)
-  inversion H1; clear H1; subst.
-  inversion H11; clear H11; subst.
-  rewrite E0_right. 
-  inversion H2; clear H2; subst. inversion H8; clear H8; subst.
-  destruct op; simplify_eq H; intro; subst a;
-  simpl in H0; destruct v1; simplify_eq H0; intro; subst v;
-  inversion H7; subst v0;
-  TrivialOp.
-  change (Vint (Int.cast8unsigned i)) with (Val.cast8unsigned (Vint i)). eauto with evalexpr.
-  change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr.
-  change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr.
-  change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr.
-  replace (Int.eq i Int.zero) with (negb (negb (Int.eq i Int.zero))).
-  eapply eval_notbool. eauto. 
-  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro; simpl.
-  rewrite H1; constructor. constructor; auto. 
-  apply negb_elim.
-  unfold Vfalse; TrivialOp. change (Vint Int.zero) with (Val.of_bool (negb true)). 
-  eapply eval_notbool. eauto. constructor. 
-  change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr.
-  (* Binary operations *)
-  inversion H1; clear H1; subst. inversion H11; clear H11; subst.
-  inversion H12; clear H12; subst. rewrite E0_right. 
-  inversion H2; clear H2; subst. inversion H9; clear H9; subst.
-  inversion H10; clear H10; subst.
-  destruct op; simplify_eq H; intro; subst a;
-  simpl in H0; destruct v2; destruct v3; simplify_eq H0; intro; try subst v;
-  inversion H7; inversion H8; subst v0; subst v1;
-  TrivialOp.
-  (* add int ptr *)
-  exists (Vptr b2 (Int.add ofs2 i)); split.
-  eauto with evalexpr. apply val_inject_ptr with x. auto.
-  subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  (* add ptr int *)
-  exists (Vptr b2 (Int.add ofs2 i0)); split.
-  eauto with evalexpr. apply val_inject_ptr with x. auto.
-  subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  (* sub ptr int *)
-  exists (Vptr b2 (Int.sub ofs2 i0)); split.
-  eauto with evalexpr. apply val_inject_ptr with x. auto.
-  subst ofs2. apply Int.sub_add_l. 
-  (* sub ptr ptr *)
-  destruct (eq_block b b0); simplify_eq H0; intro; subst v; subst b0.
-  assert (b4 = b2). congruence. subst b4.
-  exists (Vint (Int.sub ofs3 ofs2)); split. 
-  eauto with evalexpr. 
-  subst ofs2 ofs3. replace x0 with x. rewrite Int.sub_shifted. constructor.
-  congruence.
-  (* divs *)
-  generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* divu *)
-  generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* mods *)
-  generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* modu *)
-  generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* shl *)
-  caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* shr *)
-  caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* shru *)
-  caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0;
-  simplify_eq H0; intro; subst v. TrivialOp.
-  (* cmp int ptr *)
-  elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i.
-  exists v; split. eauto with evalexpr. 
-  elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor.
-  (* cmp ptr int *)
-  elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i0.
-  exists v; split. eauto with evalexpr. 
-  elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor.
+  destruct op; simpl; intros.
+  inv H; inv H0; simpl; TrivialOp.
+  inv H; inv H0; simpl; TrivialOp.
+  inv H; inv H0; simpl; TrivialOp.
+  inv H; inv H0; simpl; TrivialOp.
+  inv H0; inv H. TrivialOp. 
+  inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp.
+  inv H0; inv H; TrivialOp.
+  inv H0; inv H; TrivialOp.
+  inv H0; inv H; TrivialOp.
+  inv H; inv H0; simpl; TrivialOp.
+  inv H0; inv H; TrivialOp.
+  inv H0; inv H; TrivialOp.
+  inv H0; inv H; TrivialOp.
+Qed.
+
+(** Compatibility of [eval_binop] with respect to [val_inject]. *)
+
+Lemma eval_binop_compat:
+  forall f op v1 tv1 v2 tv2 v m tm,
+  eval_binop op v1 v2 m = Some v ->
+  val_inject f v1 tv1 ->
+  val_inject f v2 tv2 ->
+  mem_inject f m tm ->
+  exists tv,
+     eval_binop op tv1 tv2 tm = Some tv
+  /\ val_inject f v tv.
+Proof.
+  destruct op; simpl; intros.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+    repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    apply Int.sub_add_l.
+    destruct (eq_block b1 b0); inv H4. 
+    assert (b3 = b2) by congruence. subst b3. 
+    unfold eq_block; rewrite zeq_true. TrivialOp.
+    replace x0 with x by congruence. decEq. decEq. 
+    apply Int.sub_shifted.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
+    exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
   (* cmp ptr ptr *)
-  caseEq (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)); 
-  intro EQ; rewrite EQ in H0; try discriminate.
-  destruct (eq_block b b0); simplify_eq H0; intro; subst v b0.
-  assert (b4 = b2); [congruence|subst b4].
-  assert (x0 = x); [congruence|subst x0].
+  caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); 
+  intro EQ; rewrite EQ in H4; try discriminate.
+  destruct (eq_block b1 b0); inv H4.
+  assert (b3 = b2) by congruence. subst b3.
+  assert (x0 = x) by congruence. subst x0.
   elim (andb_prop _ _ EQ); intros.
-  exists (Val.of_bool (Int.cmp c ofs3 ofs2)); split.
-  eauto with evalexpr. 
-  subst ofs2 ofs3. rewrite Int.translate_cmp. 
-  apply val_inject_val_of_bool. 
+  exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split.
+  exploit (Mem.valid_pointer_inject f m tm b0 ofs0); eauto. 
+  intro VP; rewrite VP; clear VP.
+  exploit (Mem.valid_pointer_inject f m tm b0 ofs1); eauto. 
+  intro VP; rewrite VP; clear VP.
+  unfold eq_block; rewrite zeq_true; simpl.
+  decEq. decEq. rewrite Int.translate_cmp. auto. 
   eapply valid_pointer_inject_no_overflow; eauto.
   eapply valid_pointer_inject_no_overflow; eauto.
+  apply val_inject_val_of_bool. 
+  (* *)
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
 Qed.
 
 (** Correctness of [make_cast].  Note that the resulting Cminor value is
@@ -980,35 +958,28 @@ Lemma make_cast_correct:
             te tm1 (make_cast chunk a) t tm2 tv'
   /\ val_inject f (Val.load_result chunk v) tv'.
 Proof.
-  intros. destruct chunk.
+  intros. destruct chunk; simpl make_cast.
 
   exists (Val.cast8signed tv). 
-  split. apply eval_cast8signed; auto. 
-  inversion H0; simpl; constructor.
+  split. eauto with evalexpr. inversion H0; simpl; constructor.
 
   exists (Val.cast8unsigned tv). 
-  split. apply eval_cast8unsigned; auto. 
-  inversion H0; simpl; constructor.
+  split. eauto with evalexpr. inversion H0; simpl; constructor.
 
   exists (Val.cast16signed tv). 
-  split. apply eval_cast16signed; auto. 
-  inversion H0; simpl; constructor.
+  split. eauto with evalexpr. inversion H0; simpl; constructor.
 
   exists (Val.cast16unsigned tv). 
-  split. apply eval_cast16unsigned; auto. 
-  inversion H0; simpl; constructor.
+  split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists tv. 
-  split. simpl; auto.
-  inversion H0; simpl; econstructor; eauto.
+  exists tv.
+  split. auto. inversion H0; simpl; econstructor; eauto.
 
   exists (Val.singleoffloat tv). 
-  split. apply eval_singleoffloat; auto. 
-  inversion H0; simpl; constructor.
+  split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists tv. 
-  split. simpl; auto.
-  inversion H0; simpl; constructor. 
+  exists tv.
+  split. auto. inversion H0; simpl; econstructor; eauto.
 Qed.
 
 Lemma make_stackaddr_correct:
@@ -1018,7 +989,7 @@ Lemma make_stackaddr_correct:
             E0 tm (Vptr sp (Int.repr ofs)).
 Proof.
   intros; unfold make_stackaddr.
-  eapply eval_Eop. econstructor. simpl. decEq. decEq.
+  econstructor. simpl. decEq. decEq.
   rewrite Int.add_commut. apply Int.add_zero.
 Qed.
 
@@ -1030,22 +1001,10 @@ Lemma make_globaladdr_correct:
             E0 tm (Vptr b Int.zero).
 Proof.
   intros; unfold make_globaladdr.
-  eapply eval_Eop. econstructor. simpl. rewrite H. auto.
+  econstructor. simpl. rewrite H. auto.
 Qed.
 
-(** Correctness of [make_load] and [make_store]. *)
-
-Lemma make_load_correct:
-  forall sp le te tm1 a t tm2 va chunk v,
-  eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va ->
-  Mem.loadv chunk tm2 va = Some v ->
-  eval_expr tge (Vptr sp Int.zero) le
-            te tm1 (make_load chunk a)
-            t  tm2 v.
-Proof.
-  intros; unfold make_load.
-  eapply eval_load; eauto.
-Qed.
+(** Correctness of [make_store]. *)
 
 Lemma store_arg_content_inject:
   forall f sp le te tm1 a t tm2 v va chunk,
@@ -1053,25 +1012,23 @@ Lemma store_arg_content_inject:
   val_inject f v va ->
   exists vb,
   eval_expr tge (Vptr sp Int.zero) le te tm1 (store_arg chunk a) t tm2 vb  
-  /\ val_content_inject f (mem_chunk chunk) v vb.
+  /\ val_content_inject f chunk v vb.
 Proof.
   intros. 
   assert (exists vb,
     eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 vb  
-    /\ val_content_inject f (mem_chunk chunk) v vb).
+    /\ val_content_inject f chunk v vb).
   exists va; split. assumption. constructor. assumption.
-  inversion H; clear H; subst; simpl; trivial.
-  inversion H2; clear H2; subst; trivial.
-  inversion H4; clear H4; subst; trivial.
-  rewrite E0_right. rewrite E0_right in H1.
-  destruct op; trivial; destruct chunk; trivial;
-  exists v0; (split; [auto|
-  simpl in H3; inversion H3; clear H3; subst va; 
-  destruct v0; simpl in H0; inversion H0; subst; try (constructor; constructor)]).
-  apply val_content_inject_8. apply Int.cast8_unsigned_signed. 
-  apply val_content_inject_8. apply Int.cast8_unsigned_idem. 
-  apply val_content_inject_16. apply Int.cast16_unsigned_signed. 
-  apply val_content_inject_16. apply Int.cast16_unsigned_idem. 
+  destruct a; simpl store_arg; trivial;
+  destruct u; trivial;
+  destruct chunk; trivial;
+  inv H; simpl in H12; inv H12;
+  econstructor; (split; [eauto|idtac]);
+  destruct v1; simpl in H0; inv H0; try (constructor; constructor).
+  apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem.
+  apply val_content_inject_8; auto. apply Int.cast8_unsigned_signed. 
+  apply val_content_inject_16; auto. apply Int.cast16_unsigned_idem. 
+  apply val_content_inject_16; auto. apply Int.cast16_unsigned_signed. 
   apply val_content_inject_32. apply Float.singleoffloat_idem. 
 Qed.
 
@@ -1098,13 +1055,11 @@ Proof.
   intros [tv [EVAL VCINJ]].
   exploit storev_mapped_inject_1; eauto.
   intros [tm4 [STORE MEMINJ]].
-  exploit eval_store. eexact H. eexact EVAL. eauto. 
-  intro EVALSTORE.
   exists tm4. 
-  split. apply exec_Sexpr with tv. auto. 
+  split. apply exec_Sexpr with tv. eapply eval_Estore; eauto. 
   split. auto. 
   unfold storev in STORE; destruct tvaddr; try discriminate.
-  exploit store_inv; eauto. simpl. tauto.
+  eapply nextblock_store; eauto.
 Qed.
 
 (** Correctness of the variable accessors [var_get], [var_set]
@@ -1112,7 +1067,7 @@ Qed.
 
 Lemma var_get_correct:
   forall cenv id a f e te sp lo hi m cs tm b chunk v le,
-  var_get cenv id = Some a ->
+  var_get cenv id = OK a ->
   match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
   mem_inject f m tm ->
   eval_var_ref prog e id b chunk ->
@@ -1138,7 +1093,7 @@ Proof.
     unfold loadv. eexact H3. 
   intros [tv [LOAD INJ]].
   exists tv; split. 
-  eapply make_load_correct; eauto. eapply make_stackaddr_correct; eauto.
+  econstructor; eauto. eapply make_stackaddr_correct; eauto.
   auto.
   (* var_global_scalar *)
   inversion H2; [congruence|subst]. 
@@ -1151,14 +1106,14 @@ Proof.
   generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13).
   intros [tv [LOAD INJ]].
   exists tv; split. 
-  eapply make_load_correct; eauto. eapply make_globaladdr_correct; eauto.
+  econstructor; eauto. eapply make_globaladdr_correct; eauto.
   auto.
 Qed.
 
 Lemma var_addr_correct:
   forall cenv id a f e te sp lo hi m cs tm b le,
   match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
-  var_addr cenv id = Some a ->
+  var_addr cenv id = OK a ->
   eval_var_addr prog e id b ->
   exists tv,
     eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\
@@ -1196,7 +1151,7 @@ Qed.
 
 Lemma var_set_correct:
   forall cenv id rhs a f e te sp lo hi m2 cs tm2 tm1 tv b chunk v m3 t,
-  var_set cenv id rhs = Some a ->
+  var_set cenv id rhs = OK a ->
   match_callstack f (mkframe cenv e te sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 ->
   eval_expr tge (Vptr sp Int.zero) nil te tm1 rhs t tm2 tv ->
   val_inject f v tv ->
@@ -1210,7 +1165,7 @@ Lemma var_set_correct:
 Proof.
   unfold var_set; intros.
   assert (NEXTBLOCK: nextblock m3 = nextblock m2).
-    exploit store_inv; eauto. simpl; tauto.
+    eapply nextblock_store; eauto.
   inversion H0. subst.
   assert (match_var f id e m2 te sp cenv!!id). inversion H19; auto.
   inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H.
@@ -1337,7 +1292,7 @@ Proof.
       unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto.
       rewrite <- H1. omega.
       intros until delta; unfold f1, extend_inject, eq_block.
-      rewrite (high_bound_alloc _ _ b _ _ _ H).
+      rewrite (high_bound_alloc _ _ _ _ _ H b).
       case (zeq b b1); intros. 
       inversion H3. unfold sizeof; rewrite LV. omega.
       generalize (BOUND _ _ H3). omega. 
@@ -1350,7 +1305,7 @@ Proof.
     exploit IHalloc_variables; eauto.
       unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto.
       intros until delta; unfold f1, extend_inject, eq_block.
-      rewrite (high_bound_alloc _ _ b _ _ _ H).
+      rewrite (high_bound_alloc _ _ _ _ _ H b).
       case (zeq b b1); intros. discriminate.
       eapply BOUND; eauto.
     intros [f' [INCR2 [MINJ2 MATCH2]]].
@@ -1373,7 +1328,7 @@ Proof.
     unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto.
     rewrite <- H1. omega.
     intros until delta; unfold f1, extend_inject, eq_block.
-    rewrite (high_bound_alloc _ _ b _ _ _ H).
+    rewrite (high_bound_alloc _ _ _ _ _ H b).
     case (zeq b b1); intros. 
     inversion H6. unfold sizeof; rewrite LV. omega.
     generalize (BOUND _ _ H6). omega. 
@@ -1439,10 +1394,9 @@ Proof.
   intros. 
   assert (SP: sp = nextblock tm). injection H2; auto.
   unfold build_compilenv in H. 
-  eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto.
-  eapply valid_new_block; eauto.
-  rewrite (low_bound_alloc _ _ sp _ _ _ H2). apply zeq_true.
-  rewrite (high_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. 
+  eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto with mem.
+  eapply low_bound_alloc_same; eauto.
+  eapply high_bound_alloc_same; eauto.
   (* match_callstack *)
   constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto.
   constructor. 
@@ -1460,15 +1414,15 @@ Proof.
     (* me_inj *)
     intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence.
     (* me_inv *)
-    intros. exploit mi_mappedblocks; eauto. intros [A B].
+    intros. exploit mi_mappedblocks; eauto. intro A.
     elim (fresh_block_alloc _ _ _ _ _ H2 A).
     (* me_incr *)
-    intros. exploit mi_mappedblocks; eauto. intros [A B].
+    intros. exploit mi_mappedblocks; eauto. intro A.
     rewrite SP; auto.
   rewrite SP; auto.
   eapply alloc_right_inject; eauto.
   omega.
-  intros. exploit mi_mappedblocks; eauto. intros [A B].
+  intros. exploit mi_mappedblocks; eauto. unfold valid_block; intro.
   unfold block in SP; omegaContradiction.
   (* defined *)
   intros. unfold te. apply set_locals_params_defined. 
@@ -1569,7 +1523,7 @@ Proof.
   inversion H18.
   inversion NOREPET. subst hd tl.
   assert (NEXT: nextblock m1 = nextblock m).
-    exploit store_inv; eauto. simpl; tauto.
+    eapply nextblock_store; eauto.
   generalize (me_vars0 id). intro. inversion H2; subst.
   (* cenv!!id = Var_local chunk *)
   assert (b0 = b). congruence. subst b0.
@@ -1724,43 +1678,6 @@ Qed.
 
 (** * Semantic preservation for the translation *)
 
-(** These tactics simplify hypotheses of the form [f ... = Some x]. *)
-
-Ltac monadSimpl1 :=
-  match goal with
-  | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] =>
-      unfold bind at 1;
-      generalize (refl_equal F);
-      pattern F at -1 in |- *;
-      case F;
-      [ (let EQ := fresh "EQ" in
-          (intro; intro EQ;
-           try monadSimpl1))
-      | intros; discriminate ]
-  | [ |- (None = Some _) -> _ ] =>
-      intro; discriminate
-  | [ |- (Some _ = Some _) -> _ ] =>
-      let h := fresh "H" in
-      (intro h; injection h; intro; clear h)
-  end.
-
-Ltac monadSimpl :=
-  match goal with
-  | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => monadSimpl1
-  | [ |- (None = Some _) -> _ ] => monadSimpl1
-  | [ |- (Some _ = Some _) -> _ ] => monadSimpl1
-  | [ |- (?F _ _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ _ = Some _) -> _ ] => simpl F; monadSimpl1
-  | [ |- (?F _ = Some _) -> _ ] => simpl F; monadSimpl1
-  end.
-
-Ltac monadInv H :=
-  generalize H; monadSimpl.
-
 (** The proof of semantic preservation uses simulation diagrams of the
   following form:
 <<
@@ -1790,7 +1707,7 @@ Ltac monadInv H :=
 Definition eval_expr_prop
     (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop :=
   forall cenv ta f1 tle te tm1 sp lo hi cs
-  (TR: transl_expr cenv a = Some ta)
+  (TR: transl_expr cenv a = OK ta)
   (LINJ: val_list_inject f1 le tle)
   (MINJ: mem_inject f1 m1 tm1)
   (MATCH: match_callstack f1
@@ -1808,7 +1725,7 @@ Definition eval_expr_prop
 Definition eval_exprlist_prop
     (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop :=
   forall cenv tal f1 tle te tm1 sp lo hi cs
-  (TR: transl_exprlist cenv al = Some tal)
+  (TR: transl_exprlist cenv al = OK tal)
   (LINJ: val_list_inject f1 le tle)
   (MINJ: mem_inject f1 m1 tm1)
   (MATCH: match_callstack f1
@@ -1826,7 +1743,7 @@ Definition eval_exprlist_prop
 Definition eval_funcall_prop
     (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop :=
   forall tfn f1 tm1 cs targs
-  (TR: transl_fundef gce fn = Some tfn)
+  (TR: transl_fundef gce fn = OK tfn)
   (MINJ: mem_inject f1 m1 tm1)
   (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1)
   (ARGSINJ: val_list_inject f1 args targs),
@@ -1852,7 +1769,7 @@ Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop :=
 Definition exec_stmt_prop
     (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: trace) (m2: mem) (out: Csharpminor.outcome): Prop :=
   forall cenv ts f1 te1 tm1 sp lo hi cs
-  (TR: transl_stmt cenv s = Some ts)
+  (TR: transl_stmt cenv s = OK ts)
   (MINJ: mem_inject f1 m1 tm1)
   (MATCH: match_callstack f1
            (mkframe cenv e te1 sp lo hi :: cs)
@@ -1897,21 +1814,61 @@ Proof.
   exists f1; exists tm1; exists tv. intuition eauto.
 Qed.
 
-Lemma transl_expr_Eop_correct:
-   forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
-     (op : Csharpminor.operation) (al : Csharpminor.exprlist) 
-     (t: trace) (m1 : mem) (vl : list val) (v : val),
-   Csharpminor.eval_exprlist prog le e m al t m1 vl ->
-   eval_exprlist_prop le e m al t m1 vl ->
-   Csharpminor.eval_operation op vl m1 = Some v ->
-   eval_expr_prop le e m (Csharpminor.Eop op al) t m1 v.
-Proof.
-  intros; red; intros. monadInv TR; intro EQ0.
+Lemma transl_expr_Econst_correct:
+  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
+         (cst : Csharpminor.constant) (v : val),
+  Csharpminor.eval_constant cst = Some v ->
+  eval_expr_prop le e m (Csharpminor.Econst cst) E0 m v.
+Proof.
+  intros; red; intros; monadInv TR.
+  exploit transl_constant_correct; eauto.
+  intros [tv [EVAL VINJ]].
+  exists f1; exists tm1; exists tv. intuition eauto. 
+  constructor; eauto.
+Qed.
+
+Lemma transl_expr_Eunop_correct:
+  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
+         (op : unary_operation) (a : Csharpminor.expr) (t : trace)
+         (m1 : mem) (v1 v : val),
+  Csharpminor.eval_expr prog le e m a t m1 v1 ->
+  eval_expr_prop le e m a t m1 v1 ->
+  Csharpminor.eval_unop op v1 = Some v ->
+  eval_expr_prop le e m (Csharpminor.Eunop op a) t m1 v.
+Proof.
+  intros; red; intros. monadInv TR.
   exploit H0; eauto.
   intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
-  exploit make_op_correct; eauto.
-  intros [tv [EVAL2 VINJ2]].
-  exists f2; exists tm2; exists tv. intuition.
+  exploit eval_unop_compat; eauto. intros [tv [EVAL VINJ]].
+  exists f2; exists tm2; exists tv; intuition.
+  econstructor; eauto.
+Qed.
+
+Lemma transl_expr_Ebinop_correct:
+  forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem)
+         (op : binary_operation) (a1 a2 : Csharpminor.expr) (t1 : trace)
+         (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) (v2 : val)
+         (t : trace) (v : val),
+  Csharpminor.eval_expr prog le e m a1 t1 m1 v1 ->
+  eval_expr_prop le e m a1 t1 m1 v1 ->
+  Csharpminor.eval_expr prog le e m1 a2 t2 m2 v2 ->
+  eval_expr_prop le e m1 a2 t2 m2 v2 ->
+  Csharpminor.eval_binop op v1 v2 m2 = Some v ->
+  t = t1 ** t2 ->
+  eval_expr_prop le e m (Csharpminor.Ebinop op a1 a2) t m2 v.
+Proof.
+  intros; red; intros. monadInv TR.
+  exploit H0; eauto.
+  intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
+  exploit H2.
+    eauto. eapply val_list_inject_incr; eauto. eauto. eauto.  
+  intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
+  exploit eval_binop_compat.
+    eauto. eapply val_inject_incr; eauto. eauto. eauto. 
+  intros [tv [EVAL VINJ]].
+  exists f3; exists tm3; exists tv; intuition.
+  econstructor; eauto.
+  eapply inject_incr_trans; eauto.
 Qed.
 
 Lemma transl_expr_Eload_correct:
@@ -1931,7 +1888,7 @@ Proof.
   intros [tv [TLOAD VINJ]].
   exists f2; exists tm2; exists tv.
   intuition.
-  subst ta. eapply make_load_correct; eauto. 
+  econstructor; eauto.
 Qed.
 
 Lemma transl_expr_Ecall_correct:
@@ -1951,7 +1908,7 @@ Lemma transl_expr_Ecall_correct:
    t = t1 ** t2 ** t3 ->
    eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres.
 Proof.
-  intros;red;intros. monadInv TR. subst ta. 
+  intros;red;intros. monadInv TR. 
   exploit H0; eauto.
   intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
   exploit H2.
@@ -1960,18 +1917,18 @@ Proof.
   assert (tv1 = vf).
     elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3.
     rewrite Genv.find_funct_find_funct_ptr in H3. 
-    generalize (Genv.find_funct_ptr_inv H3). intro.
+    generalize (Genv.find_funct_ptr_negative H3). intro.
     assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto.
-    generalize (mg_functions _ H9 _ H8). intro.
+    generalize (mg_functions _ H7 _ H4). intro.
     rewrite VF in VINJ1. inversion VINJ1. subst vf. 
     decEq. congruence. 
-    subst ofs2. replace x with 0. reflexivity. congruence.
+    subst ofs2. replace x1 with 0. reflexivity. congruence.
   subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF].
   exploit H6; eauto.
   intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]].
   exists f4; exists tm4; exists tres. intuition.
   eapply eval_Ecall; eauto. 
-  rewrite <- H4. apply sig_preserved; auto.
+  apply sig_preserved; auto.
   apply inject_incr_trans with f2; auto. 
   apply inject_incr_trans with f3; auto.
 Qed.
@@ -1996,8 +1953,8 @@ Proof.
   intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
   exists f3; exists tm3; exists tv2.
   intuition.
-  rewrite <- H6. subst t; eapply eval_conditionalexpr_true; eauto. 
-  inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
+  eapply eval_Econdition with (b1 := true); eauto. 
+    eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; eauto.
   eapply inject_incr_trans; eauto.
 Qed.
 
@@ -2021,8 +1978,8 @@ Proof.
   intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
   exists f3; exists tm3; exists tv2.
   intuition.
-  rewrite <- H6. subst t; eapply eval_conditionalexpr_false; eauto. 
-  inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
+  eapply eval_Econdition with (b1 := false); eauto. 
+    eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; eauto.
   eapply inject_incr_trans; eauto.
 Qed.
 
@@ -2047,7 +2004,7 @@ Proof.
   intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
   exists f3; exists tm3; exists tv2.
   intuition.
-  subst ta; eapply eval_Elet; eauto.
+  eapply eval_Elet; eauto.
   eapply inject_incr_trans; eauto.
 Qed.
 
@@ -2072,7 +2029,7 @@ Proof.
   exploit val_list_inject_nth; eauto. intros [tv [A B]].
   exists f1; exists tm1; exists tv.
   intuition.
-  subst ta. eapply eval_Eletvar; auto.
+  eapply eval_Eletvar; auto.
 Qed.
 
 Lemma transl_expr_Ealloc_correct:
@@ -2095,7 +2052,7 @@ Proof.
   intros [MINJ3 INCR3].
   exists (extend_inject b (Some (tb, 0)) f2); 
   exists tm3; exists (Vptr tb Int.zero).
-  split. subst ta; econstructor; eauto.
+  split. econstructor; eauto.
   split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity.
   reflexivity.
   split. assumption.
@@ -2109,7 +2066,7 @@ Lemma transl_exprlist_Enil_correct:
 Proof.
   intros; red; intros. monadInv TR. 
   exists f1; exists tm1; exists (@nil val).
-  intuition. subst tal; constructor.
+  intuition. constructor.
 Qed.
 
 Lemma transl_exprlist_Econs_correct:
@@ -2131,7 +2088,7 @@ Proof.
     eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
   intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]].
   exists f3; exists tm3; exists (tv1 :: tv2).
-  intuition. subst tal; econstructor; eauto.
+  intuition. econstructor; eauto.
   constructor. eapply val_inject_incr; eauto. auto.
   eapply inject_incr_trans; eauto.
 Qed.
@@ -2149,15 +2106,11 @@ Lemma transl_funcall_internal_correct:
    eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres.
 Proof.
   intros; red. intros tfn f1 tm; intros.
-  generalize TR; clear TR.
-  unfold transl_fundef, transf_partial_fundef.
-  caseEq (transl_function gce f); try congruence. 
-  intros tf TR EQ. inversion EQ; clear EQ; subst tfn.
-  unfold transl_function in TR.
+  monadInv TR. generalize EQ.
+  unfold transl_function.
   caseEq (build_compilenv gce f); intros cenv stacksize CENV.
-  rewrite CENV in TR. 
-  destruct (zle stacksize Int.max_signed); try discriminate.
-  monadInv TR. clear TR. 
+  destruct (zle stacksize Int.max_signed); try congruence.
+  intro TR. monadInv TR.
   caseEq (alloc tm 0 stacksize). intros tm1 sp ALLOC.
   exploit function_entry_ok; eauto. 
   intros [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]].
@@ -2177,9 +2130,11 @@ Proof.
       exists v2; split. auto. subst vres; auto.
       contradiction.
   destruct H5 as [tvres [TOUT VINJRES]].
+  assert (outcome_free_mem tout tm3 sp = Mem.free tm3 sp).
+    inversion OUTINJ; auto.
   exists f3; exists (Mem.free tm3 sp); exists tvres.
   (* execution *)
-  split. rewrite <- H6; econstructor; simpl; eauto.
+  split. rewrite <- H5. econstructor; simpl; eauto.
   apply exec_Sseq_continue with E0 te2 tm2 t.
   exact STOREPARAM.
   eexact EXECBODY.
@@ -2195,7 +2150,7 @@ Proof.
   (* match_callstack *)
   assert (forall bl mm, nextblock (free_list mm bl) = nextblock mm).
     induction bl; intros. reflexivity. simpl. auto.
-  unfold free; simpl nextblock. rewrite H5. 
+  unfold free; simpl nextblock. rewrite H6. 
   eapply match_callstack_freelist; eauto. 
   intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega.
 Qed.
@@ -2206,8 +2161,7 @@ Lemma transl_funcall_external_correct:
   event_match ef vargs t vres ->
   eval_funcall_prop m (External ef) vargs t m vres.
 Proof.
-  intros; red; intros.
-  simpl in TR. inversion TR; clear TR; subst tfn.
+  intros; red; intros. monadInv TR. 
   exploit event_match_inject; eauto. intros [A B].
   exists f1; exists tm1; exists vres; intuition.
   constructor; auto. 
@@ -2219,7 +2173,7 @@ Lemma transl_stmt_Sskip_correct:
 Proof.
   intros; red; intros. monadInv TR. 
   exists f1; exists te1; exists tm1; exists Out_normal.
-  intuition. subst ts; constructor. constructor.
+  intuition. constructor. constructor.
 Qed.
 
 Lemma transl_stmt_Sexpr_correct:
@@ -2233,7 +2187,7 @@ Proof.
   exploit H0; eauto.
   intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
   exists f2; exists te1; exists tm2; exists Out_normal.
-  intuition. subst ts. econstructor; eauto.
+  intuition. econstructor; eauto.
   constructor.
 Qed.
 
@@ -2247,7 +2201,7 @@ Lemma transl_stmt_Sassign_correct:
    store chunk m1 b 0 v = Some m2 ->
    exec_stmt_prop e m (Csharpminor.Sassign id a) t m2 Csharpminor.Out_normal.
 Proof.
-  intros; red; intros. monadInv TR; intro EQ0. 
+  intros; red; intros. monadInv TR.
   exploit H0; eauto. 
   intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]].
   exploit var_set_correct; eauto.
@@ -2282,15 +2236,15 @@ Proof.
     eapply val_inject_incr; eauto. eauto.
   intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]].
   exists f3; exists te1; exists tm4; exists Out_normal.
-  rewrite <- H6. subst t3. intuition. 
+  intuition. 
   constructor.
   eapply inject_incr_trans; eauto.
   assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto.
   unfold storev in H3; destruct v1; try discriminate.
   inversion H4. 
   rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2).
-  eapply match_callstack_mapped; eauto. congruence. 
-  exploit store_inv; eauto. simpl; symmetry; tauto.
+  eapply match_callstack_mapped; eauto. congruence.
+  symmetry. eapply nextblock_store; eauto. 
 Qed.
 
 Lemma transl_stmt_Sseq_continue_correct:
@@ -2309,7 +2263,7 @@ Proof.
   exploit H2; eauto.
   intros [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]].
   exists f3; exists te3; exists tm3; exists tout2.
-  intuition. subst ts; eapply exec_Sseq_continue; eauto.
+  intuition. eapply exec_Sseq_continue; eauto.
   inversion OINJ1. subst tout1. auto.
   eapply inject_incr_trans; eauto.
 Qed.
@@ -2326,7 +2280,7 @@ Proof.
   exploit H0; eauto.
   intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
   exists f2; exists te2; exists tm2; exists tout1.
-  intuition. subst ts; eapply exec_Sseq_stop; eauto.
+  intuition. eapply exec_Sseq_stop; eauto.
   inversion OINJ1; subst out tout1; congruence.
 Qed.
 
@@ -2350,8 +2304,8 @@ Proof.
   intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
   exists f3; exists te3; exists tm3; exists tout.
   intuition. 
-  subst ts t. eapply exec_ifthenelse_true; eauto.
-  inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
+  eapply exec_Sifthenelse with (b1 := true); eauto.
+  eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; auto.
   eapply inject_incr_trans; eauto.
 Qed.
 
@@ -2375,8 +2329,8 @@ Proof.
   intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
   exists f3; exists te3; exists tm3; exists tout.
   intuition. 
-  subst ts t. eapply exec_ifthenelse_false; eauto.
-  inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
+  eapply exec_Sifthenelse with (b1 := false); eauto.
+  eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; auto.
   eapply inject_incr_trans; eauto.
 Qed.
 
@@ -2391,14 +2345,14 @@ Lemma transl_stmt_Sloop_loop_correct:
    t = t1 ** t2 ->
    exec_stmt_prop e m (Csharpminor.Sloop sl) t m2 out.
 Proof.
-  intros; red; intros. monadInv TR.
+  intros; red; intros. generalize TR; intro TR'; monadInv TR'.
   exploit H0; eauto.
   intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
   exploit H2; eauto.
   intros [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]].
   exists f3; exists te3; exists tm3; exists tout2.
   intuition. 
-  subst ts. eapply exec_Sloop_loop; eauto.
+  eapply exec_Sloop_loop; eauto.
   inversion OINJ1; subst tout1; eauto.
   eapply inject_incr_trans; eauto.
 Qed.
@@ -2415,7 +2369,7 @@ Proof.
   exploit H0; eauto.
   intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
   exists f2; exists te2; exists tm2; exists tout1.
-  intuition. subst ts; eapply exec_Sloop_stop; eauto.
+  intuition. eapply exec_Sloop_stop; eauto.
   inversion OINJ1; subst out tout1; congruence.
 Qed.
 
@@ -2431,7 +2385,7 @@ Proof.
   exploit H0; eauto.
   intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
   exists f2; exists te2; exists tm2; exists (outcome_block tout1).
-  intuition. subst ts; eapply exec_Sblock; eauto.
+  intuition. eapply exec_Sblock; eauto.
   inversion OINJ1; subst out tout1; simpl.
   constructor.
   destruct n; constructor.
@@ -2445,7 +2399,7 @@ Lemma transl_stmt_Sexit_correct:
 Proof.
   intros; red; intros. monadInv TR.
   exists f1; exists te1; exists tm1; exists (Out_exit n).
-  intuition. subst ts; constructor. constructor.
+  intuition. constructor. constructor.
 Qed.
 
 Lemma transl_stmt_Sswitch_correct:
@@ -2462,7 +2416,7 @@ Proof.
   intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
   exists f2; exists te1; exists tm2; 
   exists (Out_exit (switch_target n default cases)). intuition. 
-  subst ts. constructor. inversion VINJ1. subst tv1. assumption.
+  constructor. inversion VINJ1. subst tv1. assumption.
   constructor. 
 Qed.
 
@@ -2473,7 +2427,7 @@ Lemma transl_stmt_Sreturn_none_correct:
 Proof.
   intros; red; intros. monadInv TR.
   exists f1; exists te1; exists tm1; exists (Out_return None).
-  intuition. subst ts; constructor. constructor.
+  intuition. constructor. constructor.
 Qed.
 
 Lemma transl_stmt_Sreturn_some_correct:
@@ -2488,7 +2442,7 @@ Proof.
   exploit H0; eauto.
   intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
   exists f2; exists te1; exists tm2; exists (Out_return (Some tv1)).
-  intuition. subst ts; econstructor; eauto. constructor; auto.
+  intuition. econstructor; eauto. constructor; auto.
 Qed.
 
 (** We conclude by an induction over the structure of the Csharpminor
@@ -2499,7 +2453,7 @@ Lemma transl_function_correct:
    Csharpminor.eval_funcall prog m1 f vargs t m2 vres ->
    eval_funcall_prop m1 f vargs t m2 vres.
 Proof
-  (eval_funcall_ind4 prog
+  (Csharpminor.eval_funcall_ind4 prog
      eval_expr_prop
      eval_exprlist_prop
      eval_funcall_prop
@@ -2507,7 +2461,9 @@ Proof
 
      transl_expr_Evar_correct
      transl_expr_Eaddrof_correct
-     transl_expr_Eop_correct
+     transl_expr_Econst_correct
+     transl_expr_Eunop_correct
+     transl_expr_Ebinop_correct
      transl_expr_Eload_correct
      transl_expr_Ecall_correct
      transl_expr_Econdition_true_correct
@@ -2545,11 +2501,9 @@ Lemma match_globalenvs_init:
   match_globalenvs f.
 Proof.
   intros. constructor.
-  (* globalvars *)
-  (* symbols *)
   intros. split.
   unfold f. rewrite zlt_true. auto. unfold m. 
-  eapply Genv.find_symbol_inv; eauto.
+  eapply Genv.find_symbol_not_fresh; eauto.
   rewrite <- H. apply symbols_preserved.
   intros. unfold f. rewrite zlt_true. auto.
   generalize (nextblock_pos m). omega.
@@ -2566,20 +2520,10 @@ Proof.
   intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]].
   elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR].
   set (m0 := Genv.init_mem prog) in *.
-  set (f := fun b => if zlt b m0.(nextblock) then Some(b, 0) else None).
+  set (f := meminj_init m0).
   assert (MINJ0: mem_inject f m0 m0).
-    unfold f; constructor; intros.
-    apply zlt_false; auto.
-    destruct (zlt b0 (nextblock m0)); try discriminate.
-    inversion H; subst b' delta. 
-    split. auto. 
-    constructor. compute. split; congruence. left; auto. 
-    intros; omega. 
-    generalize (Genv.initmem_block_init prog b0). fold m0. intros [idata EQ].
-    rewrite EQ. simpl. apply Mem.contents_init_data_inject. 
-    destruct (zlt b1 (nextblock m0)); try discriminate.
-    destruct (zlt b2 (nextblock m0)); try discriminate.
-    left; congruence. 
+    unfold f; apply init_inject. 
+    unfold m0; apply Genv.initmem_inject_neutral.
   assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0).
     constructor. unfold f; apply match_globalenvs_init.
   fold ge in EVAL.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 4cc85559..e24430cc 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -1,6 +1,7 @@
 (** * Dynamic semantics for the Clight language *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Integers.
 Require Import Floats.
@@ -559,7 +560,7 @@ with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
  | eval_Efield_struct:   forall e m a t m1 l ofs id fList i ty delta,
       eval_lvalue e m a t m1 l ofs ->
       typeof a = Tstruct id fList ->
-      field_offset i fList = Some delta ->
+      field_offset i fList = OK delta ->
       eval_lvalue e m (Expr (Efield a i) ty)
                   t m1 l (Int.add ofs (Int.repr delta))
  | eval_Efield_union:   forall e m a t m1 l ofs id fList i ty,
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index f1d22d7e..729814ee 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -9,6 +9,7 @@ Require Import Values.
 Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
+Require Cminor.
 
 (** Abstract syntax *)
 
@@ -24,52 +25,21 @@ Require Import Globalenvs.
   Unlike in Cminor (the next intermediate language of the back-end),
   Csharpminor local variables reside in memory, and their address can
   be taken using [Eaddrof] expressions.
+*)
+
+Inductive constant : Set :=
+  | Ointconst: int -> constant          (**r integer constant *)
+  | Ofloatconst: float -> constant.     (**r floating-point constant *)
 
-  Another difference with Cminor is that Csharpminor is entirely 
-  processor-neutral. In particular, Csharpminor uses a standard set of
-  operations: it does not reflect processor-specific operations nor
-  addressing modes. *)
-
-Inductive operation : Set :=
-  | Ointconst: int -> operation         (**r integer constant *)
-  | Ofloatconst: float -> operation     (**r floating-point constant *)
-  | Ocast8unsigned: operation           (**r 8-bit zero extension  *)
-  | Ocast8signed: operation             (**r 8-bit sign extension  *)
-  | Ocast16unsigned: operation          (**r 16-bit zero extension  *)
-  | Ocast16signed: operation            (**r 16-bit sign extension *)
-  | Onotbool: operation                 (**r boolean negation  *)
-  | Onotint: operation                  (**r bitwise complement  *)
-  | Oadd: operation                     (**r integer addition *)
-  | Osub: operation                     (**r integer subtraction *)
-  | Omul: operation                     (**r integer multiplication *)
-  | Odiv: operation                     (**r integer signed division *)
-  | Odivu: operation                    (**r integer unsigned division *)
-  | Omod: operation                     (**r integer signed modulus *)
-  | Omodu: operation                    (**r integer unsigned modulus *)
-  | Oand: operation                     (**r bitwise ``and'' *)
-  | Oor: operation                      (**r bitwise ``or'' *)
-  | Oxor: operation                     (**r bitwise ``xor'' *)
-  | Oshl: operation                     (**r left shift *)
-  | Oshr: operation                     (**r right signed shift *)
-  | Oshru: operation                    (**r right unsigned shift *)
-  | Onegf: operation                    (**r float opposite *)
-  | Oabsf: operation                    (**r float absolute value *)
-  | Oaddf: operation                    (**r float addition *)
-  | Osubf: operation                    (**r float subtraction *)
-  | Omulf: operation                    (**r float multiplication *)
-  | Odivf: operation                    (**r float division *)
-  | Osingleoffloat: operation           (**r float truncation *)
-  | Ointoffloat: operation              (**r integer to float *)
-  | Ofloatofint: operation              (**r float to signed integer *)
-  | Ofloatofintu: operation             (**r float to unsigned integer *)
-  | Ocmp: comparison -> operation       (**r integer signed comparison *)
-  | Ocmpu: comparison -> operation      (**r integer unsigned comparison *)
-  | Ocmpf: comparison -> operation.     (**r float comparison *)
+Definition unary_operation : Set := Cminor.unary_operation.
+Definition binary_operation : Set := Cminor.binary_operation.
 
 Inductive expr : Set :=
   | Evar : ident -> expr                (**r reading a scalar variable  *)
   | Eaddrof : ident -> expr             (**r taking the address of a variable *)
-  | Eop : operation -> exprlist -> expr (**r arithmetic operation *)
+  | Econst : constant -> expr
+  | Eunop : unary_operation -> expr -> expr
+  | Ebinop : binary_operation -> expr -> expr -> expr
   | Eload : memory_chunk -> expr -> expr (**r memory read *)
   | Ecall : signature -> expr -> exprlist -> expr (**r function call *)
   | Econdition : expr -> expr -> expr -> expr (**r conditional expression *)
@@ -202,78 +172,15 @@ Definition global_var_env (p: program): gvarenv :=
 
 (** Evaluation of operator applications. *)
 
-Definition eval_compare_null (c: comparison) (n: int) : option val :=
-  if Int.eq n Int.zero 
-  then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end
-  else None.
-
-Definition eval_operation (op: operation) (vl: list val) (m: mem): option val :=
-  match op, vl with
-  | Ointconst n, nil => Some (Vint n)
-  | Ofloatconst n, nil => Some (Vfloat n)
-  | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1))
-  | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1))
-  | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1))
-  | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1))
-  | Onotbool, Vint n1 :: nil => Some (Val.of_bool (Int.eq n1 Int.zero))
-  | Onotbool, Vptr b1 n1 :: nil => Some (Vfalse)
-  | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1))
-  | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
-  | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
-  | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
-  | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None
-  | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2))
-  | Odiv, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2))
-  | Odivu, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-  | Omod, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
-  | Omodu, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
-  | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2))
-  | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2))
-  | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2))
-  | Oshl, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
-  | Oshr, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
-  | Oshru, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
-  | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
-  | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1))
-  | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2))
-  | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
-  | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
-  | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
-  | Osingleoffloat, Vfloat f1 :: nil =>
-      Some (Vfloat (Float.singleoffloat f1))
-  | Ointoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intoffloat f1))
-  | Ofloatofint, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofintu n1))
-  | Ocmp c, Vint n1 :: Vint n2 :: nil =>
-      Some (Val.of_bool(Int.cmp c n1 n2))
-  | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if valid_pointer m b1 (Int.signed n1)
-      && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None
-      else
-        None
-  | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2
-  | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1
-  | Ocmpu c, Vint n1 :: Vint n2 :: nil =>
-      Some (Val.of_bool(Int.cmpu c n1 n2))
-  | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil =>
-      Some (Val.of_bool (Float.cmp c f1 f2))
-  | _, _ => None
+Definition eval_constant (cst: constant) : option val :=
+  match cst with
+  | Ointconst n => Some (Vint n)
+  | Ofloatconst n => Some (Vfloat n)
   end.
 
+Definition eval_unop := Cminor.eval_unop.
+Definition eval_binop := Cminor.eval_binop.
+
 (** Allocation of local variables at function entry.  Each variable is
   bound to the reference to a fresh block of the appropriate size. *)
 
@@ -361,11 +268,22 @@ Inductive eval_expr:
       forall le e m id b,
       eval_var_addr e id b ->
       eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero)
-  | eval_Eop:
-      forall le e m op al t m1 vl v,
-      eval_exprlist le e m al t m1 vl ->
-      eval_operation op vl m1 = Some v ->
-      eval_expr le e m (Eop op al) t m1 v
+  | eval_Econst:
+      forall le e m cst v,
+      eval_constant cst = Some v ->
+      eval_expr le e m (Econst cst) E0 m v
+  | eval_Eunop:
+      forall le e m op a t m1 v1 v,
+      eval_expr le e m a t m1 v1 ->
+      eval_unop op v1 = Some v ->
+      eval_expr le e m (Eunop op a) t m1 v
+  | eval_Ebinop:
+      forall le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v,
+      eval_expr le e m a1 t1 m1 v1 ->
+      eval_expr le e m1 a2 t2 m2 v2 ->
+      eval_binop op v1 v2 m2 = Some v ->
+      t = t1 ** t2 ->
+      eval_expr le e m (Ebinop op a1 a2) t m2 v
   | eval_Eload:
       forall le e m chunk a t m1 v1 v,
       eval_expr le e m a t m1 v1 ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 664c6fc4..5ab685db 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -1,19 +1,14 @@
 Require Import Coqlib.
+Require Import Errors.
 Require Import Integers.
 Require Import Floats.
 Require Import AST.
 Require Import Csyntax.
+Require Import Cminor.
 Require Import Csharpminor.
 
-(** The error monad *)
-
-Definition bind (A B: Set) (f: option A) (g: A -> option B) :=
-  match f with None => None | Some x => g x end.
-
-Implicit Arguments bind [A B].
-
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X ident, A at level 100, B at level 200).
+Open Local Scope string_scope.
+Open Local Scope error_monad_scope.
 
 (** ** Operations on C types *)
 
@@ -22,28 +17,28 @@ Definition signature_of_function (f: Csyntax.function) : signature :=
    (typlist_of_typelist (type_of_params (Csyntax.fn_params f)))
    (opttyp_of_type (Csyntax.fn_return f)).
 
-Definition chunk_of_type (ty: type): option memory_chunk :=
+Definition chunk_of_type (ty: type): res memory_chunk :=
   match access_mode ty with
-  | By_value chunk => Some chunk
-  | _ => None
+  | By_value chunk => OK chunk
+  | _ => Error (msg "Cshmgen.chunk_of_type")
   end.
 
-Definition var_kind_of_type (ty: type): option var_kind :=
+Definition var_kind_of_type (ty: type): res var_kind :=
   match ty with
-  | Tint I8 Signed => Some(Vscalar Mint8signed)
-  | Tint I8 Unsigned => Some(Vscalar Mint8unsigned)
-  | Tint I16 Signed => Some(Vscalar Mint16signed)
-  | Tint I16 Unsigned => Some(Vscalar Mint16unsigned)
-  | Tint I32 _ => Some(Vscalar Mint32)
-  | Tfloat F32 => Some(Vscalar Mfloat32)
-  | Tfloat F64 => Some(Vscalar Mfloat64)
-  | Tvoid => None
-  | Tpointer _ => Some(Vscalar Mint32)
-  | Tarray _ _ => Some(Varray (Csyntax.sizeof ty))
-  | Tfunction _ _ => None
-  | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty))
-  | Tunion _ fList => Some(Varray (Csyntax.sizeof ty))
-  | Tcomp_ptr _ => Some(Vscalar Mint32)
+  | Tint I8 Signed => OK(Vscalar Mint8signed)
+  | Tint I8 Unsigned => OK(Vscalar Mint8unsigned)
+  | Tint I16 Signed => OK(Vscalar Mint16signed)
+  | Tint I16 Unsigned => OK(Vscalar Mint16unsigned)
+  | Tint I32 _ => OK(Vscalar Mint32)
+  | Tfloat F32 => OK(Vscalar Mfloat32)
+  | Tfloat F64 => OK(Vscalar Mfloat64)
+  | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)")
+  | Tpointer _ => OK(Vscalar Mint32)
+  | Tarray _ _ => OK(Varray (Csyntax.sizeof ty))
+  | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)")
+  | Tstruct _ fList => OK(Varray (Csyntax.sizeof ty))
+  | Tunion _ fList => OK(Varray (Csyntax.sizeof ty))
+  | Tcomp_ptr _ => OK(Vscalar Mint32)
 end.
   
 (** ** Csharpminor constructors *)
@@ -60,19 +55,14 @@ end.
    denoting a case where the operation is not defined at the given types.
 *)
 
-Definition make_intconst (n: int) :=  Eop (Ointconst n) Enil.
-
-Definition make_floatconst (f: float) :=  Eop (Ofloatconst f) Enil.
-
-Definition make_unop (op: operation) (e: expr) :=  Eop op (Econs e Enil).
+Definition make_intconst (n: int) :=  Econst (Ointconst n).
 
-Definition make_binop (op: operation) (e1 e2: expr) :=
-    Eop op (Econs e1 (Econs e2 Enil)).
+Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
 Definition make_floatofint (e: expr) (sg: signedness) :=
   match sg with
-  | Signed => make_unop Ofloatofint e
-  | Unsigned => make_unop Ofloatofintu e
+  | Signed => Eunop Ofloatofint e
+  | Unsigned => Eunop Ofloatofintu e
   end.
 
 (* [make_boolean e ty] returns a Csharpminor expression that evaluates
@@ -84,98 +74,98 @@ Definition make_floatofint (e: expr) (sg: signedness) :=
 *)
 Definition make_boolean (e: expr) (ty: type) :=
   match ty with
-  | Tfloat _ => make_binop (Ocmpf Cne) e (make_floatconst Float.zero)
+  | Tfloat _ => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
   | _ => e
   end.
 
 Definition make_neg (e: expr) (ty: type) :=
   match ty with
-  | Tint _ _ => Some (make_binop Osub (make_intconst Int.zero) e)
-  | Tfloat _ => Some (make_unop Onegf e)
-  | _ => None
+  | Tint _ _ => OK (Eunop Onegint e)
+  | Tfloat _ => OK (Eunop Onegf e)
+  | _ => Error (msg "Cshmgen.make_neg")
   end.
 
 Definition make_notbool (e: expr) (ty: type) :=
   match ty with
-  | Tfloat _ => make_binop (Ocmpf Ceq) e (make_floatconst Float.zero)
-  | _ => make_unop Onotbool e
+  | Tfloat _ => Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)
+  | _ => Eunop Onotbool e
   end.
 
 Definition make_notint (e: expr) (ty: type) :=
-  make_unop Onotint e.
+  Eunop Onotint e.
 
 Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
-  | add_case_ii => Some (make_binop Oadd e1 e2)
-  | add_case_ff => Some (make_binop Oaddf e1 e2)
+  | add_case_ii => OK (Ebinop Oadd e1 e2)
+  | add_case_ff => OK (Ebinop Oaddf e1 e2)
   | add_case_pi ty =>
       let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
-      Some (make_binop Oadd e1 (make_binop Omul n e2))
-  | add_default => None
+      OK (Ebinop Oadd e1 (Ebinop Omul n e2))
+  | add_default => Error (msg "Cshmgen.make_add")
   end.
 
 Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
-  | sub_case_ii => Some (make_binop Osub e1 e2)
-  | sub_case_ff => Some (make_binop Osubf e1 e2)
+  | sub_case_ii => OK (Ebinop Osub e1 e2)
+  | sub_case_ff => OK (Ebinop Osubf e1 e2)
   | sub_case_pi ty =>
       let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
-      Some (make_binop Osub e1 (make_binop Omul n e2))
+      OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
-      Some (make_binop Odivu (make_binop Osub e1 e2) n)
-  | sub_default => None
+      OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
+  | sub_default => Error (msg "Cshmgen.make_sub")
   end.
 
 Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_mul ty1 ty2 with
-  | mul_case_ii => Some (make_binop Omul e1 e2)
-  | mul_case_ff => Some (make_binop Omulf e1 e2)
-  | mul_default => None
+  | mul_case_ii => OK (Ebinop Omul e1 e2)
+  | mul_case_ff => OK (Ebinop Omulf e1 e2)
+  | mul_default => Error (msg "Cshmgen.make_mul")
   end.
 
 Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_div ty1 ty2 with
-  | div_case_I32unsi => Some (make_binop Odivu e1 e2)
-  | div_case_ii => Some (make_binop Odiv e1 e2)
-  | div_case_ff => Some (make_binop Odivf e1 e2)
-  | div_default => None
+  | div_case_I32unsi => OK (Ebinop Odivu e1 e2)
+  | div_case_ii => OK (Ebinop Odiv e1 e2)
+  | div_case_ff => OK (Ebinop Odivf e1 e2)
+  | div_default => Error (msg "Cshmgen.make_div")
   end.
 
 Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_mod ty1 ty2 with
-  | mod_case_I32unsi => Some (make_binop Omodu e1 e2)
-  | mod_case_ii=> Some (make_binop Omod e1 e2)
-  | mod_default => None
+  | mod_case_I32unsi => OK (Ebinop Omodu e1 e2)
+  | mod_case_ii=> OK (Ebinop Omod e1 e2)
+  | mod_default => Error (msg "Cshmgen.make_mod")
   end.
 
 Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  Some(make_binop Oand e1 e2).
+  OK(Ebinop Oand e1 e2).
 
 Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  Some(make_binop Oor e1 e2).
+  OK(Ebinop Oor e1 e2).
 
 Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  Some(make_binop Oxor e1 e2).
+  OK(Ebinop Oxor e1 e2).
 
 Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  Some(make_binop Oshl e1 e2).
+  OK(Ebinop Oshl e1 e2).
 
 Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_shr ty1 ty2 with
-  | shr_case_I32unsi => Some (make_binop Oshru e1 e2)
-  | shr_case_ii=> Some (make_binop Oshr e1 e2)
-  | shr_default => None
+  | shr_case_I32unsi => OK (Ebinop Oshru e1 e2)
+  | shr_case_ii=> OK (Ebinop Oshr e1 e2)
+  | shr_default => Error (msg "Cshmgen.make_shr")
   end.
 
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
-  | cmp_case_I32unsi => Some (make_binop (Ocmpu c) e1 e2)
-  | cmp_case_ii => Some (make_binop (Ocmp c) e1 e2)
-  | cmp_case_ff => Some (make_binop (Ocmpf c) e1 e2)
-  | cmp_case_pi => Some (make_binop (Ocmp c) e1 e2)
-  | cmp_case_pp => Some (make_binop (Ocmp c) e1 e2)
-  | cmp_default => None
+  | cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2)
+  | cmp_case_ii => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
+  | cmp_case_pi => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_case_pp => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_default => Error (msg "Cshmgen.make_shr")
   end.
 
 Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -206,17 +196,17 @@ Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 Definition make_cast1 (from to: type) (e: expr) :=
   match from, to with
   | Tint _ uns, Tfloat _ => make_floatofint e uns
-  | Tfloat _, Tint _ _ => make_unop Ointoffloat e
+  | Tfloat _, Tint _ _ => Eunop Ointoffloat e
   | _, _ => e
   end.
 
 Definition make_cast2 (from to: type) (e: expr) :=
   match to with
-  | Tint I8 Signed => make_unop Ocast8signed e  
-  | Tint I8 Unsigned => make_unop Ocast8unsigned e  
-  | Tint I16 Signed => make_unop Ocast16signed e  
-  | Tint I16 Unsigned => make_unop Ocast16unsigned e  
-  | Tfloat F32 => make_unop Osingleoffloat e
+  | Tint I8 Signed => Eunop Ocast8signed e  
+  | Tint I8 Unsigned => Eunop Ocast8unsigned e  
+  | Tint I16 Signed => Eunop Ocast16signed e  
+  | Tint I16 Unsigned => Eunop Ocast16unsigned e  
+  | Tfloat F32 => Eunop Osingleoffloat e
   | _ => e
   end.
 
@@ -231,9 +221,9 @@ Definition make_cast (from to: type) (e: expr) :=
 
 Definition make_load (addr: expr) (ty_res: type) :=
   match (access_mode ty_res) with
-  | By_value chunk => Some (Eload chunk addr)
-  | By_reference => Some addr
-  | By_nothing => None
+  | By_value chunk => OK (Eload chunk addr)
+  | By_reference => OK addr
+  | By_nothing => Error (msg "Cshmgen.make_load")
   end.
 
 (* [make_store addr ty_res rhs ty_rhs] stores the value of the
@@ -243,8 +233,8 @@ Definition make_load (addr: expr) (ty_res: type) :=
 
 Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
   match access_mode ty with
-  | By_value chunk => Some (Sstore chunk addr rhs)
-  | _ => None
+  | By_value chunk => OK (Sstore chunk addr rhs)
+  | _ => Error (msg "Cshmgen.make_store")
   end.
 
 (** ** Reading and writing variables *)
@@ -258,9 +248,9 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
 
 Definition var_get (id: ident) (ty: type) :=
   match access_mode ty with
-  | By_value chunk => Some (Evar id)
-  | By_reference => Some (Eaddrof id)
-  | _ => None
+  | By_value chunk => OK (Evar id)
+  | By_reference => OK (Eaddrof id)
+  | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil)
   end.
 
 (* [var_set id ty rhs] stores the value of the Csharpminor
@@ -269,21 +259,22 @@ Definition var_get (id: ident) (ty: type) :=
 
 Definition var_set (id: ident) (ty: type) (rhs: expr) :=
   match access_mode ty with
-  | By_value chunk => Some (Sassign id rhs)
-  | _ => None
+  | By_value chunk => OK (Sassign id rhs)
+  | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil)
   end.
 
 (** ** Translation of operators *)
 
-Definition transl_unop (op: unary_operation) (a: expr) (ta: type) : option expr :=
+Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr :=
   match op with
-  | Csyntax.Onotbool => Some(make_notbool a ta)
-  | Csyntax.Onotint => Some(make_notint a ta)
+  | Csyntax.Onotbool => OK(make_notbool a ta)
+  | Csyntax.Onotint => OK(make_notint a ta)
   | Csyntax.Oneg => make_neg a ta
   end.
 
-Definition transl_binop (op: binary_operation) (a: expr) (ta: type)
-                                  (b: expr) (tb: type) : option expr :=
+Definition transl_binop (op: Csyntax.binary_operation)
+                        (a: expr) (ta: type)
+                        (b: expr) (tb: type) : res expr :=
   match op with
   | Csyntax.Oadd => make_add a ta b tb
   | Csyntax.Osub => make_sub a ta b tb
@@ -315,12 +306,12 @@ Definition transl_binop (op: binary_operation) (a: expr) (ta: type)
    a || b    --->    a ? 1 : (b ? 1 : 0)
 *)
 
-Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
+Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
   match a with
   | Expr (Csyntax.Econst_int n) _ =>
-      Some(make_intconst n)
+      OK(make_intconst n)
   | Expr (Csyntax.Econst_float n) _ =>
-      Some(make_floatconst n)
+      OK(make_floatconst n)
   | Expr (Csyntax.Evar id) ty =>
       var_get id ty
   | Expr (Csyntax.Ederef b) _ =>
@@ -337,7 +328,7 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
       transl_binop op tb (typeof b) tc (typeof c)
   | Expr (Csyntax.Ecast ty b) _ =>
       do tb <- transl_expr b;
-      Some (make_cast (typeof b) ty tb)
+      OK (make_cast (typeof b) ty tb)
   | Expr (Csyntax.Eindex b c) ty =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
@@ -348,31 +339,33 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
       | fun_case_f args res =>
           do tb <- transl_expr b;
           do tcl <- transl_exprlist cl;
-          Some(Ecall (signature_of_type args res) tb tcl)
-      | _ => None
+          OK(Ecall (signature_of_type args res) tb tcl)
+      | _ =>
+          Error(msg "Cshmgen.transl_expr(call)")
       end 
   | Expr (Csyntax.Eandbool b c) _ =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
-      Some(make_andbool tb (typeof b) tc (typeof c))
+      OK(make_andbool tb (typeof b) tc (typeof c))
   | Expr (Csyntax.Eorbool b c) _ =>
       do tb <- transl_expr b;
       do tc <- transl_expr c;
-      Some(make_orbool tb (typeof b) tc (typeof c))
+      OK(make_orbool tb (typeof b) tc (typeof c))
   | Expr (Csyntax.Esizeof ty) _ =>
-      Some(make_intconst (Int.repr (Csyntax.sizeof ty)))
+      OK(make_intconst (Int.repr (Csyntax.sizeof ty)))
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
       | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
           make_load
-            (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+            (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
             ty
       | Tunion _ fld =>
           do tb <- transl_lvalue b;
           make_load tb ty
-      | _ => None
+      | _ =>
+          Error(msg "Cshmgen.transl_expr(field)")
       end
   end
 
@@ -381,10 +374,10 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
    where the value of [a] is stored.
 *)
 
-with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
+with transl_lvalue (a: Csyntax.expr) {struct a} : res expr :=
   match a with
   | Expr (Csyntax.Evar id) _ =>
-      Some (Eaddrof id)
+      OK (Eaddrof id)
   | Expr (Csyntax.Ederef b) _ =>
       transl_expr b
   | Expr (Csyntax.Eindex b c) _ =>
@@ -396,25 +389,27 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
       | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
-          Some (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+          OK (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
       | Tunion _ fld =>
           transl_lvalue b
-      | _ => None
+      | _ =>
+          Error(msg "Cshmgen.transl_lvalue(field)")
       end
-  | _ => None
+  | _ => 
+      Error(msg "Cshmgen.transl_lvalue")
   end
 
 (* [transl_exprlist al] returns a list of Csharpminor expressions
    that compute the values of the list [al] of Csyntax expressions.
    Used for function applications. *)
 
-with transl_exprlist (al: Csyntax.exprlist): option exprlist :=
+with transl_exprlist (al: Csyntax.exprlist): res exprlist :=
   match al with
-  | Csyntax.Enil => Some Enil
+  | Csyntax.Enil => OK Enil
   | Csyntax.Econs a1 a2 =>
       do ta1 <- transl_expr a1;
       do ta2 <- transl_exprlist a2;
-      Some (Econs ta1 ta2)
+      OK (Econs ta1 ta2)
   end.
 
 (** ** Translation of statements *)
@@ -431,9 +426,9 @@ Definition is_variable (e: Csyntax.expr) : option ident :=
    value of the CabsCoq expression [e] and performs an [exit 0] if [e]
    evaluates to false.
 *)
-Definition exit_if_false (e: Csyntax.expr) : option stmt :=
+Definition exit_if_false (e: Csyntax.expr) : res stmt :=
   do te <- transl_expr e;
-  Some(Sifthenelse
+  OK(Sifthenelse
         (make_boolean te (typeof e))
         Sskip
         (Sexit 0%nat)).
@@ -497,13 +492,13 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int
   | LScase ni _ rem => (ni, k) :: switch_table rem (k+1)
   end.
 
-Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : option stmt :=
+Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt :=
   match s with
   | Csyntax.Sskip =>
-      Some Sskip
+      OK Sskip
   | Csyntax.Sexpr e =>
       do te <- transl_expr e;
-      Some (Sexpr te)
+      OK (Sexpr te)
   | Csyntax.Sassign b c =>
       match (is_variable b) with
       | Some id =>
@@ -517,35 +512,35 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o
   | Csyntax.Ssequence s1 s2 =>
       do ts1 <- transl_statement nbrk ncnt s1;
       do ts2 <- transl_statement nbrk ncnt s2;
-      Some (Sseq ts1 ts2)
+      OK (Sseq ts1 ts2)
   | Csyntax.Sifthenelse e s1 s2 =>
       do te <- transl_expr e;
       do ts1 <- transl_statement nbrk ncnt s1;
       do ts2 <- transl_statement nbrk ncnt s2;
-      Some (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
+      OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
   | Csyntax.Swhile e s1 =>
       do te <- exit_if_false e;
       do ts1 <- transl_statement 1%nat 0%nat s1;
-      Some (Sblock (Sloop (Sseq te (Sblock ts1))))
+      OK (Sblock (Sloop (Sseq te (Sblock ts1))))
   | Csyntax.Sdowhile e s1 =>
       do te <- exit_if_false e;
       do ts1 <- transl_statement 1%nat 0%nat s1;
-      Some (Sblock (Sloop (Sseq (Sblock ts1) te)))
+      OK (Sblock (Sloop (Sseq (Sblock ts1) te)))
   | Csyntax.Sfor e1 e2 e3 s1 =>
       do te1 <- transl_statement nbrk ncnt e1;
       do te2 <- exit_if_false e2;
       do te3 <- transl_statement nbrk ncnt e3;
       do ts1 <- transl_statement 1%nat 0%nat s1;
-      Some (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
+      OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
   | Csyntax.Sbreak =>
-      Some (Sexit nbrk)
+      OK (Sexit nbrk)
   | Csyntax.Scontinue =>
-      Some (Sexit ncnt)
+      OK (Sexit ncnt)
   | Csyntax.Sreturn (Some e) =>
       do te <- transl_expr e;
-      Some (Sreturn (Some te))
+      OK (Sreturn (Some te))
   | Csyntax.Sreturn None =>
-      Some (Sreturn None)
+      OK (Sreturn None)
   | Csyntax.Sswitch e sl =>
       let cases := switch_table sl 0 in
       let ncases := List.length cases in
@@ -554,11 +549,11 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o
   end
 
 with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
-                     {struct sl}: option stmt :=
+                     {struct sl}: res stmt :=
   match sl with
   | LSdefault s =>
       do ts <- transl_statement nbrk ncnt s;
-      Some (Sblock (Sseq body ts))
+      OK (Sblock (Sseq body ts))
   | LScase _ s rem =>
       do ts <- transl_statement nbrk ncnt s;
       transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts))
@@ -566,28 +561,31 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
 
 (*** Translation of functions *)
 
+Definition prefix_var_name (id: ident) : errmsg :=
+  MSG "In local variable " :: CTX id :: MSG ":\n" :: nil.
+
 Definition transl_params (l: list (ident * type)) :=
-   AST.map_partial chunk_of_type l.
+   AST.map_partial prefix_var_name chunk_of_type l.
 Definition transl_vars (l: list (ident * type)) :=
-   AST.map_partial var_kind_of_type l.
+   AST.map_partial prefix_var_name var_kind_of_type l.
 
-Definition transl_function (f: Csyntax.function) : option function :=
+Definition transl_function (f: Csyntax.function) : res function :=
   do tparams <- transl_params (Csyntax.fn_params f);
   do tvars <- transl_vars (Csyntax.fn_vars f);
   do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f);
-  Some (mkfunction (signature_of_function f) tparams tvars tbody).
+  OK (mkfunction (signature_of_function f) tparams tvars tbody).
 
-Definition transl_fundef (f: Csyntax.fundef) : option fundef :=
+Definition transl_fundef (f: Csyntax.fundef) : res fundef :=
   match f with
   | Csyntax.Internal g => 
-      do tg <- transl_function g; Some(AST.Internal tg)
+      do tg <- transl_function g; OK(AST.Internal tg)
   | Csyntax.External id args res =>
-      Some(AST.External (external_function id args res))
+      OK(AST.External (external_function id args res))
   end.
 
 (** ** Translation of programs *)
 
 Definition transl_globvar (ty: type) := var_kind_of_type ty.
 
-Definition transl_program (p: Csyntax.program) : option program :=
+Definition transl_program (p: Csyntax.program) : res program :=
   transform_partial_program2 transl_fundef transl_globvar p.
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index bee07824..7ffd156c 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -1,6 +1,7 @@
 (** * Correctness of the C front end, part 1: syntactic properties *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Integers.
 Require Import Floats.
@@ -12,64 +13,28 @@ Require Import Globalenvs.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Ctyping.
+Require Import Cminor.
 Require Import Csharpminor.
 Require Import Cshmgen.
 
-(** Monadic simplification *)
-
-Ltac monadSimpl1 :=
-  match goal with
-  | [ |- (bind ?F ?G = Some ?X) -> _ ] =>
-      unfold bind at 1;
-      generalize (refl_equal F);
-      pattern F at -1 in |- *;
-      case F;
-      [ (let EQ := fresh "EQ" in
-           (intro; intro EQ; try monadSimpl1))
-      | intro; intro; discriminate ]
-  | [ |- (None = Some _) -> _ ] =>
-      intro; discriminate
-  | [ |- (Some _ = Some _) -> _ ] =>
-      let h := fresh "H" in
-      (intro h; injection h; intro; clear h)
-  | [ |- (_ = Some _) -> _ ] =>
-      let EQ := fresh "EQ" in intro EQ
-  end.
-
-Ltac monadSimpl :=
-  match goal with
-  | [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1
-  | [ |- (None = Some _) -> _ ] => monadSimpl1
-  | [ |- (Some _ = Some _) -> _ ] => monadSimpl1
-  | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  | [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  | [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  | [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  | [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
-  end.
-
-Ltac monadInv H :=
-  generalize H; monadSimpl.
-
 (** Operations on types *)
 
 Lemma transl_fundef_sig1:
   forall f tf args res,
-  transl_fundef f = Some tf ->
+  transl_fundef f = OK tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res ->
   funsig tf = signature_of_type args res.
 Proof.
   intros. destruct f; monadInv H. 
-  monadInv EQ. rewrite <- H2. rewrite <- H3. simpl. 
+  monadInv EQ. simpl.  
   simpl in H0. inversion H0. reflexivity. 
-  rewrite <- H2. simpl. 
+  simpl. 
   simpl in H0. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
   forall f tf args res,
-  transl_fundef f = Some tf ->
+  transl_fundef f = OK tf ->
   type_of_fundef f = Tfunction args res ->
   funsig tf = signature_of_type args res.
 Proof.
@@ -80,7 +45,7 @@ Qed.
 Lemma var_kind_by_value:
   forall ty chunk,
   access_mode ty = By_value chunk ->
-  var_kind_of_type ty = Some(Vscalar chunk).
+  var_kind_of_type ty = OK(Vscalar chunk).
 Proof.
   intros ty chunk; destruct ty; simpl; try congruence.
   destruct i; try congruence; destruct s; congruence.
@@ -89,7 +54,7 @@ Qed.
 
 Lemma sizeof_var_kind_of_type:
   forall ty vk,
-  var_kind_of_type ty = Some vk ->
+  var_kind_of_type ty = OK vk ->
   Csharpminor.sizeof vk = Csyntax.sizeof ty.
 Proof.
   intros ty vk.
@@ -103,35 +68,35 @@ Qed.
 (** ** Some properties of the translation functions *)
 
 Lemma map_partial_names:
-  forall (A B: Set) (f: A -> option B)
+  forall (A B: Set) (f: A -> res B)
          (l: list (ident * A)) (tl: list (ident * B)),
-  map_partial f l = Some tl ->
+  map_partial prefix_var_name f l = OK tl ->
   List.map (@fst ident B) tl = List.map (@fst ident A) l.
 Proof.
   induction l; simpl.
   intros. inversion H. reflexivity.
   intro tl. destruct a as [id x]. destruct (f x); try congruence.
-  caseEq (map_partial f l); intros; try congruence.
-  inversion H0; subst tl. simpl. decEq. auto.
+  caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence.
+  inv H0. simpl. decEq. auto.
 Qed.
    
 Lemma map_partial_append:
-  forall (A B: Set) (f: A -> option B)
+  forall (A B: Set) (f: A -> res B)
          (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
-  map_partial f l1 = Some tl1 ->
-  map_partial f l2 = Some tl2 ->
-  map_partial f (l1 ++ l2) = Some (tl1 ++ tl2).
+  map_partial prefix_var_name f l1 = OK tl1 ->
+  map_partial prefix_var_name f l2 = OK tl2 ->
+  map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2).
 Proof.
   induction l1; intros until tl2; simpl.
   intros. inversion H. simpl; auto.
   destruct a as [id x]. destruct (f x); try congruence.
-  caseEq (map_partial f l1); intros; try congruence.
-  inversion H0. rewrite (IHl1 _ _ _ H H1). auto.
+  caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence.
+  inv H0. rewrite (IHl1 _ _ _ H H1). auto.
 Qed.
  
 Lemma transl_params_names:
   forall vars tvars,
-  transl_params vars = Some tvars ->
+  transl_params vars = OK tvars ->
   List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars.
 Proof.
   exact (map_partial_names _ _ chunk_of_type).
@@ -139,7 +104,7 @@ Qed.
 
 Lemma transl_vars_names:
   forall vars tvars,
-  transl_vars vars = Some tvars ->
+  transl_vars vars = OK tvars ->
   List.map (@fst ident var_kind) tvars = Ctyping.var_names vars.
 Proof.
   exact (map_partial_names _ _ var_kind_of_type).
@@ -148,8 +113,8 @@ Qed.
 Lemma transl_names_norepet:
   forall params vars sg tparams tvars body,
   list_norepet (var_names params ++ var_names vars) ->
-  transl_params params = Some tparams ->
-  transl_vars vars = Some tvars ->
+  transl_params params = OK tparams ->
+  transl_vars vars = OK tvars ->
   let f := Csharpminor.mkfunction sg tparams tvars body in
   list_norepet (fn_params_names f ++ fn_vars_names f).
 Proof.
@@ -161,35 +126,35 @@ Qed.
 
 Lemma transl_vars_append:
   forall l1 l2 tl1 tl2,
-  transl_vars l1 = Some tl1 -> transl_vars l2 = Some tl2 ->
-  transl_vars (l1 ++ l2) = Some (tl1 ++ tl2).
+  transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 ->
+  transl_vars (l1 ++ l2) = OK (tl1 ++ tl2).
 Proof.
   exact (map_partial_append _ _ var_kind_of_type).
 Qed.
 
 Lemma transl_params_vars:
   forall params tparams,
-  transl_params params = Some tparams ->
+  transl_params params = OK tparams ->
   transl_vars params =
-  Some (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams).
+  OK (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams).
 Proof.
   induction params; intro tparams; simpl.
   intros. inversion H. reflexivity.
   destruct a as [id x]. 
   unfold chunk_of_type. caseEq (access_mode x); try congruence.
   intros chunk AM. 
-  caseEq (transl_params params); intros; try congruence.
-  inversion H0. 
+  caseEq (transl_params params); simpl; intros; try congruence.
+  inv H0. 
   rewrite (var_kind_by_value _ _ AM). 
   rewrite (IHparams _ H). reflexivity.
 Qed.
 
 Lemma transl_fn_variables:
   forall params vars sg tparams tvars body,
-  transl_params params = Some tparams ->
-  transl_vars vars = Some tvars ->
+  transl_params params = OK tparams ->
+  transl_vars vars = OK tvars ->
   let f := Csharpminor.mkfunction sg tparams tvars body in
-  transl_vars (params ++ vars) = Some (fn_variables f).
+  transl_vars (params ++ vars) = OK (fn_variables f).
 Proof.
   intros. 
   generalize (transl_params_vars _ _ H); intro.
@@ -212,35 +177,36 @@ Qed.
 Lemma transl_expr_lvalue:
   forall ge e m1 a ty t m2 loc ofs ta,
   Csem.eval_lvalue ge e m1 (Expr a ty) t m2 loc ofs ->
-  transl_expr (Expr a ty) = Some ta ->
-  (exists id, a = Csyntax.Evar id /\ var_get id ty = Some ta) \/
-  (exists tb, transl_lvalue (Expr a ty) = Some tb /\
-              make_load tb ty = Some ta).
+  transl_expr (Expr a ty) = OK ta ->
+  (exists id, a = Csyntax.Evar id /\ var_get id ty = OK ta) \/
+  (exists tb, transl_lvalue (Expr a ty) = OK tb /\
+              make_load tb ty = OK ta).
 Proof.
   intros. inversion H; subst; clear H; simpl in H0.
   left; exists id; auto.
   left; exists id; auto.
-  monadInv H0. right. exists e0; split; auto. 
-  simpl. monadInv H0. right. exists e2; split; auto. 
-  simpl. rewrite H6 in H0. rewrite H6. 
-  monadInv H0. right. 
-  exists (make_binop Oadd e0 (make_intconst (Int.repr z))). split; auto.
-  simpl. rewrite H10 in H0. rewrite H10. 
-  monadInv H0. right. 
-  exists e0; auto.
+  monadInv H0. right. exists x; split; auto. 
+  simpl. monadInv H0. right. exists x1; split; auto. 
+  simpl. rewrite EQ; rewrite EQ1. simpl. auto.
+  rewrite H6 in H0. monadInv H0. right.  
+  exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto.
+  simpl. rewrite H6. rewrite EQ. rewrite EQ1. auto.
+  rewrite H10 in H0. monadInv H0. right.
+  exists x; split; auto. 
+  simpl. rewrite H10. auto.
 Qed.
 
 Lemma transl_stmt_Sfor_start:
   forall nbrk ncnt s1 e2 s3 s4 ts,
-  transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = Some ts ->
+  transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = OK ts ->
   exists ts1, exists ts2,
     ts = Sseq ts1 ts2
-  /\ transl_statement nbrk ncnt s1 = Some ts1
-  /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = Some (Sseq Sskip ts2).
+  /\ transl_statement nbrk ncnt s1 = OK ts1
+  /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK (Sseq Sskip ts2).
 Proof.
-  intros. monadInv H. simpl. 
-  exists s; exists (Sblock (Sloop (Sseq s0 (Sseq (Sblock s5) s2)))).
-  intuition.
+  intros. monadInv H. econstructor; econstructor.
+  split. reflexivity. split. auto. simpl.
+  rewrite EQ1; rewrite EQ0; rewrite EQ2; auto.
 Qed.
 
 (** Properties related to switch constructs *)
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 0458bd56..8e2ce303 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -1,6 +1,7 @@
 (** * Correctness of the C front end, part 2: Csharpminor construction functions *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Integers.
 Require Import Floats.
@@ -12,6 +13,7 @@ Require Import Globalenvs.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Ctyping.
+Require Import Cminor.
 Require Import Csharpminor.
 Require Import Cshmgen.
 Require Import Cshmgenproof1.
@@ -25,14 +27,14 @@ Variable tprog: Csharpminor.program.
 Lemma transl_lblstmts_exit:
   forall e m1 t m2 sl body n tsl nbrk ncnt,
   exec_stmt tprog e m1 body t m2 (Out_exit (lblstmts_length sl + n)) ->
-  transl_lblstmts nbrk ncnt sl body = Some tsl ->
+  transl_lblstmts nbrk ncnt sl body = OK tsl ->
   exec_stmt tprog e m1 tsl t m2 (outcome_block (Out_exit n)).
 Proof.
   induction sl; intros.
   simpl in H; simpl in H0; monadInv H0. 
-  rewrite <- H2. constructor. apply exec_Sseq_stop. auto. congruence.
+  constructor. apply exec_Sseq_stop. auto. congruence.
   simpl in H; simpl in H0; monadInv H0.
-  eapply IHsl with (body := Sblock (Sseq body s0)); eauto.
+  eapply IHsl with (body := Sblock (Sseq body x)); eauto.
   change (Out_exit (lblstmts_length sl + n))
     with (outcome_block (Out_exit (S (lblstmts_length sl + n)))).
   constructor. apply exec_Sseq_stop. auto. congruence.
@@ -41,15 +43,15 @@ Qed.
 Lemma transl_lblstmts_return:
   forall e m1 t m2 sl body optv tsl nbrk ncnt,
   exec_stmt tprog e m1 body t m2 (Out_return optv) ->
-  transl_lblstmts nbrk ncnt sl body = Some tsl ->
+  transl_lblstmts nbrk ncnt sl body = OK tsl ->
   exec_stmt tprog e m1 tsl t m2 (Out_return optv).
 Proof.
   induction sl; intros.
   simpl in H; simpl in H0; monadInv H0. 
-  rewrite <- H2. change (Out_return optv) with (outcome_block (Out_return optv)).
+  change (Out_return optv) with (outcome_block (Out_return optv)).
   constructor. apply exec_Sseq_stop. auto. congruence.
   simpl in H; simpl in H0; monadInv H0.
-  eapply IHsl with (body := Sblock (Sseq body s0)); eauto.
+  eapply IHsl with (body := Sblock (Sseq body x)); eauto.
   change (Out_return optv) with (outcome_block (Out_return optv)).
   constructor. apply exec_Sseq_stop. auto. congruence.
 Qed.
@@ -61,41 +63,18 @@ Lemma make_intconst_correct:
   forall n le e m1,
   Csharpminor.eval_expr tprog le e m1 (make_intconst n) E0 m1 (Vint n).
 Proof.
-  intros. unfold make_intconst. econstructor. constructor. reflexivity. 
+  intros. unfold make_intconst. econstructor. constructor.  
 Qed.
 
 Lemma make_floatconst_correct:
   forall n le e m1,
   Csharpminor.eval_expr tprog le e m1 (make_floatconst n) E0 m1 (Vfloat n).
 Proof.
-  intros. unfold make_floatconst. econstructor. constructor. reflexivity. 
-Qed.
-
-Lemma make_unop_correct:
-  forall op le e m1 a ta m2 va v,
-  Csharpminor.eval_expr tprog le e m1 a ta m2 va ->
-  eval_operation op (va :: nil) m2 = Some v ->
-  Csharpminor.eval_expr tprog le e m1 (make_unop op a) ta m2 v.
-Proof.
-  intros. unfold make_unop. econstructor. econstructor. eauto. constructor.
-  traceEq. auto.
-Qed.
-
-Lemma make_binop_correct:
-  forall op le e m1 a ta m2 va b tb m3 vb t v,
-  Csharpminor.eval_expr tprog le e m1 a ta m2 va ->
-  Csharpminor.eval_expr tprog le e m2 b tb m3 vb ->
-  eval_operation op (va :: vb :: nil) m3 = Some v ->
-  t = ta ** tb ->
-  Csharpminor.eval_expr tprog le e m1 (make_binop op a b) t m3 v.
-Proof.
-  intros. unfold make_binop. 
-  econstructor. econstructor. eauto. econstructor. eauto. constructor.
-  reflexivity. traceEq. auto.
+  intros. unfold make_floatconst. econstructor. constructor.  
 Qed.
 
 Hint Resolve make_intconst_correct make_floatconst_correct
-             make_unop_correct make_binop_correct: cshm.
+             eval_Eunop eval_Ebinop: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
 Remark Vtrue_is_true: Val.is_true Vtrue.
@@ -120,7 +99,7 @@ Proof.
   destruct ty; simpl;
   try (exists v; intuition; inversion VTRUE; simpl; auto; fail).
   exists Vtrue; split.
-  eapply make_binop_correct; eauto with cshm. 
+  econstructor; eauto with cshm. 
   inversion VTRUE; simpl. 
   replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)).
   rewrite Float.eq_zero_false. reflexivity. auto.
@@ -140,7 +119,7 @@ Proof.
   destruct ty; simpl;
   try (exists v; intuition; inversion VFALSE; simpl; auto; fail).
   exists Vfalse; split.
-  eapply make_binop_correct; eauto with cshm. 
+  econstructor; eauto with cshm. 
   inversion VFALSE; simpl. 
   replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)).
   rewrite Float.eq_zero_true. reflexivity. 
@@ -151,13 +130,13 @@ Qed.
 Lemma make_neg_correct:
   forall a tya c ta va v le e m1 m2,
   sem_neg va tya = Some v ->
-  make_neg a tya = Some c ->  
+  make_neg a tya = OK c ->  
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m1 c ta m2 v.
 Proof.
   intros until m2; intro SEM. unfold make_neg. 
   functional inversion SEM; intros.
-  inversion H4. eapply make_binop_correct; eauto with cshm.
+  inversion H4. econstructor; eauto with cshm.
   inversion H4. eauto with cshm.
 Qed.
 
@@ -186,21 +165,21 @@ Proof.
 Qed.
 
 Definition binary_constructor_correct
-    (make: expr -> type -> expr -> type -> option expr)
+    (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> type -> val -> type -> option val): Prop :=
   forall a tya b tyb c ta va tb vb v le e m1 m2 m3,
   sem va tya vb tyb = Some v ->
-  make a tya b tyb = Some c ->  
+  make a tya b tyb = OK c ->  
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m2 b tb m3 vb ->
   eval_expr tprog le e m1 c (ta ** tb) m3 v.
 
 Definition binary_constructor_correct'
-    (make: expr -> type -> expr -> type -> option expr)
+    (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> val -> option val): Prop :=
   forall a tya b tyb c ta va tb vb v le e m1 m2 m3,
   sem va vb = Some v ->
-  make a tya b tyb = Some c ->  
+  make a tya b tyb = OK c ->  
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m2 b tb m3 vb ->
   eval_expr tprog le e m1 c (ta ** tb) m3 v.
@@ -212,8 +191,8 @@ Proof.
   inversion H7. eauto with cshm. 
   inversion H7. eauto with cshm.
   inversion H7. 
-  eapply make_binop_correct. eauto. 
-  eapply make_binop_correct. eauto with cshm. eauto.
+  econstructor. eauto. 
+  econstructor. eauto with cshm. eauto.
   simpl. reflexivity. reflexivity. 
   simpl. reflexivity. traceEq.
 Qed.
@@ -223,12 +202,12 @@ Proof.
   red; intros until m3. intro SEM. unfold make_sub. 
   functional inversion SEM; rewrite H0; intros;
   inversion H7; eauto with cshm. 
-  eapply make_binop_correct. eauto. 
-  eapply make_binop_correct. eauto with cshm. eauto.
+  econstructor. eauto. 
+  econstructor. eauto with cshm. eauto.
   simpl. reflexivity. reflexivity. 
   simpl. reflexivity. traceEq.
-  inversion H9. eapply make_binop_correct. 
-  eapply make_binop_correct; eauto. 
+  inversion H9. econstructor. 
+  econstructor; eauto. 
   simpl. unfold eq_block; rewrite H3. reflexivity.
   eauto with cshm. simpl. rewrite H8. reflexivity. traceEq.
 Qed.
@@ -244,9 +223,9 @@ Lemma make_div_correct: binary_constructor_correct make_div sem_div.
 Proof.
   red; intros until m3. intro SEM. unfold make_div. 
   functional inversion SEM; rewrite H0; intros.
-  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  inversion H8. econstructor; eauto with cshm. 
   simpl. rewrite H7; auto.
-  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  inversion H8. econstructor; eauto with cshm. 
   simpl. rewrite H7; auto.
   inversion H7; eauto with cshm. 
 Qed.
@@ -254,9 +233,9 @@ Qed.
 Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
   red; intros until m3. intro SEM. unfold make_mod. 
   functional inversion SEM; rewrite H0; intros.
-  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  inversion H8. econstructor; eauto with cshm. 
   simpl. rewrite H7; auto.
-  inversion H8. eapply make_binop_correct; eauto with cshm. 
+  inversion H8. econstructor; eauto with cshm. 
   simpl. rewrite H7; auto.
 Qed.
 
@@ -285,7 +264,7 @@ Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl.
 Proof.
   red; intros until m3. intro SEM. unfold make_shl. 
   functional inversion SEM. intros. inversion H5. 
-  eapply make_binop_correct; eauto with cshm. 
+  econstructor; eauto with cshm. 
   simpl. rewrite H4. auto.
 Qed.
 
@@ -293,16 +272,16 @@ Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
 Proof.
   red; intros until m3. intro SEM. unfold make_shr. 
   functional inversion SEM; intros; rewrite H0 in H8; inversion H8.
-  eapply make_binop_correct; eauto with cshm.
+  econstructor; eauto with cshm.
   simpl; rewrite H7; auto.
-  eapply make_binop_correct; eauto with cshm.
+  econstructor; eauto with cshm.
   simpl; rewrite H7; auto.
 Qed.
 
 Lemma make_cmp_correct:
   forall cmp a tya b tyb c ta va tb vb v le e m1 m2 m3,
   sem_cmp cmp va tya vb tyb m3 = Some v ->
-  make_cmp cmp a tya b tyb = Some c ->  
+  make_cmp cmp a tya b tyb = OK c ->  
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m2 b tb m3 vb ->
   eval_expr tprog le e m1 c (ta ** tb) m3 v.
@@ -312,16 +291,16 @@ Proof.
   inversion H8. eauto with cshm.
   inversion H8. eauto with cshm.
   inversion H8. eauto with cshm.
-  inversion H9. eapply make_binop_correct; eauto with cshm.
+  inversion H9. econstructor; eauto with cshm.
   simpl. functional inversion H; subst; unfold eval_compare_null;
   rewrite H8; auto.
-  inversion H10. eapply make_binop_correct; eauto with cshm.
+  inversion H10. econstructor; eauto with cshm.
   simpl. rewrite H3. unfold eq_block; rewrite H9. auto.
 Qed.
 
 Lemma transl_unop_correct:
   forall op a tya c ta va v le e m1 m2, 
-  transl_unop op a tya = Some c ->
+  transl_unop op a tya = OK c ->
   sem_unary_operation op va tya = Some v ->
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m1 c ta m2 v.
@@ -334,7 +313,7 @@ Qed.
 
 Lemma transl_binop_correct:
 forall op a tya b tyb c ta va tb vb v le e m1 m2 m3,
-  transl_binop op a tya b tyb = Some c ->  
+  transl_binop op a tya b tyb = OK c ->  
   sem_binary_operation op va tya vb tyb m3 = Some v ->
   eval_expr tprog le e m1 a ta m2 va ->
   eval_expr tprog le e m2 b tb m3 vb ->
@@ -365,7 +344,7 @@ Lemma make_cast_correct:
    cast v ty1 ty2 v' ->
    eval_expr tprog le e m1 (make_cast ty1 ty2 a) t m2 v'.
 Proof.
-  unfold make_cast, make_cast1, make_cast2, make_unop.
+  unfold make_cast, make_cast1, make_cast2.
   intros until v'; intros EVAL CAST.
   inversion CAST; clear CAST; subst.
   (* cast_int_int *)
@@ -373,7 +352,7 @@ Proof.
   (* cast_float_int *)
     destruct sz2; destruct si2; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_int_float *)
-    destruct sz2; destruct si1; unfold make_floatofint, make_unop; repeat econstructor; eauto with cshm; simpl; auto.
+    destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_float_float *)
     destruct sz2; repeat econstructor; eauto with cshm.
   (* neutral, ptr *)
@@ -384,7 +363,7 @@ Qed.
 
 Lemma make_load_correct:
   forall addr ty code b ofs v le e m1 t m2,
-  make_load addr ty = Some code ->
+  make_load addr ty = OK code ->
   eval_expr tprog le e m1 addr t m2 (Vptr b ofs) ->
   load_value_of_type ty m2 b ofs = Some v ->
   eval_expr tprog le e m1 code t m2 v.
@@ -400,7 +379,7 @@ Qed.
 
 Lemma make_store_correct:
   forall addr ty rhs code e m1 t1 m2 b ofs t2 m3 v m4,
-  make_store addr ty rhs = Some code ->
+  make_store addr ty rhs = OK code ->
   eval_expr tprog nil e m1 addr t1 m2 (Vptr b ofs) ->
   eval_expr tprog nil e m2 rhs t2 m3 v ->
   store_value_of_type ty m3 b ofs v = Some m4 ->
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 497286b3..c8b9caf0 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1,6 +1,7 @@
 (** * Correctness of the C front end, part 3: semantic preservation *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Integers.
 Require Import Floats.
@@ -12,6 +13,7 @@ Require Import Globalenvs.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Ctyping.
+Require Import Cminor.
 Require Import Csharpminor.
 Require Import Cshmgen.
 Require Import Cshmgenproof1.
@@ -22,40 +24,26 @@ Section CORRECTNESS.
 Variable prog: Csyntax.program.
 Variable tprog: Csharpminor.program.
 Hypothesis WTPROG: wt_program prog.
-Hypothesis TRANSL: transl_program prog = Some tprog.
+Hypothesis TRANSL: transl_program prog = OK tprog.
 
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros. unfold ge, tge. 
-  apply Genv.find_symbol_transf_partial2 with transl_fundef transl_globvar.
-  auto.
-Qed.
+Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL).
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
-  exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf.
-Proof.
-  intros. 
-  generalize (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL H).
-  intros [A B]. 
-  destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
-Qed.
+  exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
+Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL).
 
 Lemma function_ptr_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf.
-Proof.
-  intros. 
-  generalize (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL H).
-  intros [A B]. 
-  destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
-Qed.
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL).
 
 Lemma functions_well_typed:
   forall v f,
@@ -119,7 +107,7 @@ Proof.
 Qed.
 
 Lemma match_var_kind_of_type:
-  forall ty vk, var_kind_of_type ty = Some vk -> match_var_kind ty vk.
+  forall ty vk, var_kind_of_type ty = OK vk -> match_var_kind ty vk.
 Proof.
   intros; red. 
   caseEq (access_mode ty); auto.
@@ -131,7 +119,7 @@ Lemma match_env_alloc_variables:
   Csem.alloc_variables e1 m1 vars e2 m2 lb ->
   forall tyenv te1 tvars,
   match_env tyenv e1 te1 ->
-  transl_vars vars = Some tvars ->
+  transl_vars vars = OK tvars ->
   exists te2,
   Csharpminor.alloc_variables te1 m1 tvars te2 m2 lb
   /\ match_env (Ctyping.add_vars tyenv vars) e2 te2.
@@ -140,8 +128,8 @@ Proof.
   simpl in H0. inversion H0; subst; clear H0. 
   exists te1; split. constructor. simpl. auto.
   generalize H2. simpl. 
-  caseEq (var_kind_of_type ty); [intros vk VK | congruence].
-  caseEq (transl_vars vars); [intros tvrs TVARS | congruence].
+  caseEq (var_kind_of_type ty); simpl; [intros vk VK | congruence].
+  caseEq (transl_vars vars); simpl; [intros tvrs TVARS | congruence].
   intro EQ; inversion EQ; subst tvars; clear EQ.
   set (te2 := PTree.set id (b1, vk) te1).
   assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2).
@@ -168,14 +156,14 @@ Lemma bind_parameters_match_rec:
   forall tyenv te tvars,
   (forall id ty, In (id, ty) vars -> tyenv!id = Some ty) ->
   match_env tyenv e te ->
-  transl_params vars = Some tvars ->
+  transl_params vars = OK tvars ->
   Csharpminor.bind_parameters te m1 tvars vals m2.
 Proof.
   induction 1; intros.
   simpl in H1. inversion H1. constructor.
   generalize H4; clear H4; simpl. 
-  caseEq (chunk_of_type ty); [intros chunk CHK | congruence].
-  caseEq (transl_params params); [intros tparams TPARAMS | congruence].
+  caseEq (chunk_of_type ty); simpl; [intros chunk CHK | congruence].
+  caseEq (transl_params params); simpl; [intros tparams TPARAMS | congruence].
   intro EQ; inversion EQ; clear EQ; subst tvars.
   generalize CHK. unfold chunk_of_type. 
   caseEq (access_mode ty); intros; try discriminate.
@@ -215,7 +203,7 @@ Lemma bind_parameters_match:
   Csem.bind_parameters e m1 params vals m2 ->
   list_norepet (var_names params ++ var_names vars) ->
   match_env (Ctyping.add_vars tyenv (params ++ vars)) e te ->
-  transl_params params = Some tvars ->
+  transl_params params = OK tvars ->
   Csharpminor.bind_parameters te m1 tvars vals m2.
 Proof.
   intros. 
@@ -273,14 +261,14 @@ Qed.
 Lemma add_global_var_match_globalenv:
   forall vars tenv gv tvars,
   match_globalenv tenv gv ->
-  map_partial transl_globvar vars = Some tvars ->
+  map_partial AST.prefix_var_name transl_globvar vars = OK tvars ->
   match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars).
 Proof.
   induction vars; simpl.
   intros. inversion H0. assumption.
   destruct a as [[id init] ty]. intros until tvars; intro.
-  caseEq (transl_globvar ty); try congruence. intros vk VK. 
-  caseEq (map_partial transl_globvar vars); try congruence. intros tvars' EQ1 EQ2.
+  caseEq (transl_globvar ty); simpl; try congruence. intros vk VK. 
+  caseEq (map_partial AST.prefix_var_name transl_globvar vars); simpl; try congruence. intros tvars' EQ1 EQ2.
   inversion EQ2; clear EQ2. simpl. 
   apply IHvars; auto.
   red. intros until chunk. repeat rewrite PTree.gsspec. 
@@ -299,7 +287,7 @@ Proof.
   unfold global_typenv.
   apply add_global_var_match_globalenv.
   apply add_global_funs_match_global_env. 
-  unfold transl_program in TRANSL. functional inversion TRANSL. auto.
+  unfold transl_program in TRANSL. monadInv TRANSL. auto.
 Qed.
 
 (** ** Variable accessors *)
@@ -309,7 +297,7 @@ Lemma var_get_correct:
   Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) E0 m loc ofs ->
   load_value_of_type ty m loc ofs = Some v ->
   wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
-  var_get id ty = Some code ->
+  var_get id ty = OK code ->
   match_env tyenv e te ->
   eval_expr tprog le te m code E0 m v.
 Proof.
@@ -356,7 +344,7 @@ Lemma var_set_correct:
   Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs ->
   store_value_of_type ty m2 loc ofs v = Some m3 ->
   wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
-  var_set id ty rhs = Some code ->
+  var_set id ty rhs = OK code ->
   match_env tyenv e te ->
   eval_expr tprog nil te m1 rhs t2 m2 v ->
   exec_stmt tprog te m code (t1 ** t2) m3 Out_normal.
@@ -394,7 +382,7 @@ Definition eval_expr_prop
     (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop :=
   forall tyenv ta te tle
     (WT: wt_expr tyenv a)
-    (TR: transl_expr a = Some ta)
+    (TR: transl_expr a = OK ta)
     (MENV: match_env tyenv e te),
   Csharpminor.eval_expr tprog tle te m1 ta t m2 v.
 
@@ -403,7 +391,7 @@ Definition eval_lvalue_prop
     (m2: mem) (b: block) (ofs: int) : Prop :=
   forall tyenv ta te tle
     (WT: wt_expr tyenv a)
-    (TR: transl_lvalue a = Some ta)
+    (TR: transl_lvalue a = OK ta)
     (MENV: match_env tyenv e te),
   Csharpminor.eval_expr tprog tle te m1 ta t m2 (Vptr b ofs).
 
@@ -412,7 +400,7 @@ Definition eval_exprlist_prop
     (m2: mem) (vl: list val) : Prop :=
   forall tyenv tal te tle
     (WT: wt_exprlist tyenv al)
-    (TR: transl_exprlist al = Some tal)
+    (TR: transl_exprlist al = OK tal)
     (MENV: match_env tyenv e te),
   Csharpminor.eval_exprlist tprog tle te m1 tal t m2 vl.
 
@@ -429,7 +417,7 @@ Definition exec_stmt_prop
     (m2: mem) (out: Csem.outcome) : Prop :=
   forall tyenv nbrk ncnt ts te
     (WT: wt_stmt tyenv s)
-    (TR: transl_statement nbrk ncnt s = Some ts)   
+    (TR: transl_statement nbrk ncnt s = OK ts)   
     (MENV: match_env tyenv e te),
   Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out).
 
@@ -440,7 +428,7 @@ Definition exec_lblstmts_prop
     (WT: wt_lblstmts tyenv s)
     (TR: transl_lblstmts (lblstmts_length s)
                          (1 + lblstmts_length s + ncnt)
-                         s body = Some ts)   
+                         s body = OK ts)   
     (MENV: match_env tyenv e te)
     (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal),
   Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 
@@ -451,7 +439,7 @@ Definition eval_funcall_prop
     (t: trace) (m2: mem) (res: val) : Prop :=
   forall tf
     (WT: wt_fundef (global_typenv prog) f)
-    (TR: transl_fundef f = Some tf),
+    (TR: transl_fundef f = OK tf),
    Csharpminor.eval_funcall tprog m1 tf params t m2 res.
 
 (*
@@ -465,7 +453,7 @@ Lemma transl_Econst_int_correct:
         eval_expr_prop e m (Expr (Econst_int i) ty) E0 m (Vint i)).
 Proof.
   intros; red; intros.
-  monadInv TR. subst ta. apply make_intconst_correct.
+  monadInv TR. apply make_intconst_correct.
 Qed.
 
 Lemma transl_Econst_float_correct:
@@ -473,7 +461,7 @@ Lemma transl_Econst_float_correct:
         eval_expr_prop e m (Expr (Econst_float f0) ty) E0 m (Vfloat f0)).
 Proof.
   intros; red; intros.
-  monadInv TR. subst ta. apply make_floatconst_correct.
+  monadInv TR. apply make_floatconst_correct.
 Qed.
 
 Lemma transl_Elvalue_correct:
@@ -512,16 +500,16 @@ Lemma transl_Esizeof_correct:
         eval_expr_prop e m (Expr (Esizeof ty') ty) E0 m
           (Vint (Int.repr (Csyntax.sizeof ty')))).
 Proof.
-  intros; red; intros. monadInv TR. subst ta. apply make_intconst_correct. 
+  intros; red; intros. monadInv TR. apply make_intconst_correct. 
 Qed.
 
 Lemma transl_Eunop_correct:
-       (forall (e : Csem.env) (m : mem) (op : unary_operation)
+       (forall (e : Csem.env) (m : mem) (op : Csyntax.unary_operation)
           (a : Csyntax.expr) (ty : type) (t : trace) (m1 : mem) (v1 v : val),
         Csem.eval_expr ge e m a t m1 v1 ->
         eval_expr_prop e m a t m1 v1 ->
         sem_unary_operation op v1 (typeof a) = Some v ->
-        eval_expr_prop e m (Expr (Eunop op a) ty) t m1 v).
+        eval_expr_prop e m (Expr (Csyntax.Eunop op a) ty) t m1 v).
 Proof.
   intros; red; intros.
   inversion WT; clear WT; subst.
@@ -530,7 +518,7 @@ Proof.
 Qed.
 
 Lemma transl_Ebinop_correct:
-       (forall (e : Csem.env) (m : mem) (op : binary_operation)
+       (forall (e : Csem.env) (m : mem) (op : Csyntax.binary_operation)
           (a1 a2 : Csyntax.expr) (ty : type) (t1 : trace) (m1 : mem)
           (v1 : val) (t2 : trace) (m2 : mem) (v2 v : val),
         Csem.eval_expr ge e m a1 t1 m1 v1 ->
@@ -538,7 +526,7 @@ Lemma transl_Ebinop_correct:
         Csem.eval_expr ge e m1 a2 t2 m2 v2 ->
         eval_expr_prop e m1 a2 t2 m2 v2 ->
         sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v ->
-        eval_expr_prop e m (Expr (Ebinop op a1 a2) ty) (t1 ** t2) m2 v).
+        eval_expr_prop e m (Expr (Csyntax.Ebinop op a1 a2) ty) (t1 ** t2) m2 v).
 Proof.
   intros; red; intros.
   inversion WT; clear WT; subst.
@@ -555,7 +543,7 @@ Lemma transl_Eorbool_1_correct:
         eval_expr_prop e m (Expr (Eorbool a1 a2) ty) t m1 Vtrue).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
-  rewrite <- H3; unfold make_orbool.
+  unfold make_orbool.
   exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]].
   eapply eval_Econdition_true; eauto.
   unfold Vtrue; apply make_intconst_correct. traceEq.
@@ -574,7 +562,7 @@ Lemma transl_Eorbool_2_correct:
         eval_expr_prop e m (Expr (Eorbool a1 a2) ty) (t1 ** t2) m2 v).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
-  rewrite <- H6; unfold make_orbool.
+  unfold make_orbool.
   exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]].
   eapply eval_Econdition_false; eauto.
   inversion H4; subst.
@@ -595,7 +583,7 @@ Lemma transl_Eandbool_1_correct:
         eval_expr_prop e m (Expr (Eandbool a1 a2) ty) t m1 Vfalse).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
-  rewrite <- H3; unfold make_andbool.
+  unfold make_andbool.
   exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]].
   eapply eval_Econdition_false; eauto.
   unfold Vfalse; apply make_intconst_correct. traceEq.
@@ -614,7 +602,7 @@ Lemma transl_Eandbool_2_correct:
         eval_expr_prop e m (Expr (Eandbool a1 a2) ty) (t1 ** t2) m2 v).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
-  rewrite <- H6; unfold make_andbool.
+  unfold make_andbool.
   exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]].
   eapply eval_Econdition_true; eauto.
   inversion H4; subst.
@@ -634,7 +622,7 @@ Lemma transl_Ecast_correct:
         cast v1 (typeof a) ty v ->
         eval_expr_prop e m (Expr (Ecast ty a) ty) t m1 v).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   eapply make_cast_correct; eauto.
 Qed.
 
@@ -660,7 +648,7 @@ Proof.
   caseEq (classify_fun (typeof a)).
   2: intros; rewrite H7 in TR; discriminate.
   intros targs tres EQ. rewrite EQ in TR. 
-  monadInv TR. clear TR. subst ta.
+  monadInv TR. 
   rewrite <- H4 in EQ.
   exploit functions_translated; eauto. intros [tf [FIND TRL]].
   econstructor.
@@ -679,7 +667,7 @@ Lemma transl_Evar_local_correct:
         e ! id = Some l ->
         eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]].
   econstructor. eapply eval_var_addr_local. eauto. 
 Qed.
@@ -691,7 +679,7 @@ Lemma transl_Evar_global_correct:
         Genv.find_symbol ge id = Some l ->
         eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero).
 Proof.
-  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta.
+  intros; red; intros. inversion WT; clear WT; subst. monadInv TR. 
   exploit (me_global _ _ _ MENV); eauto. intros [A B].
   econstructor. eapply eval_var_addr_global. eauto. 
   rewrite symbols_preserved. auto.
@@ -730,13 +718,13 @@ Lemma transl_Efield_struct_correct:
         eval_lvalue ge e m a t m1 l ofs ->
         eval_lvalue_prop e m a t m1 l ofs ->
         typeof a = Tstruct id fList ->
-        field_offset i fList = Some delta ->
+        field_offset i fList = OK delta ->
         eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l
           (Int.add ofs (Int.repr delta))).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. 
   simpl in TR. rewrite H1 in TR. monadInv TR.
-  rewrite <- H5. eapply make_binop_correct; eauto.
+  econstructor; eauto.
   apply make_intconst_correct. 
   simpl. congruence. traceEq.
 Qed.
@@ -758,7 +746,7 @@ Lemma transl_Enil_correct:
        (forall (e : Csem.env) (m : mem),
         eval_exprlist_prop e m Csyntax.Enil E0 m nil).
 Proof.
-  intros; red; intros. monadInv TR. subst tal. constructor.
+  intros; red; intros. monadInv TR. constructor.
 Qed.
 
 Lemma transl_Econs_correct:
@@ -772,14 +760,14 @@ Lemma transl_Econs_correct:
         eval_exprlist_prop e m (Csyntax.Econs a bl) (t1 ** t2) m2 (v :: vl)).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. 
-  subst tal. econstructor; eauto. 
+  econstructor; eauto. 
 Qed.
 
 Lemma transl_Sskip_correct:
        (forall (e : Csem.env) (m : mem),
         exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal).
 Proof.
-  intros; red; intros. monadInv TR. subst ts. simpl. constructor.
+  intros; red; intros. monadInv TR. simpl. constructor.
 Qed.
 
 Lemma transl_Sexpr_correct:
@@ -790,8 +778,7 @@ Lemma transl_Sexpr_correct:
         exec_stmt_prop e m (Csyntax.Sexpr a) t m1 Csem.Out_normal).
 Proof.
   intros; red; intros; simpl. inversion WT; clear WT; subst. 
-  monadInv TR. subst ts. 
-  econstructor; eauto.
+  monadInv TR. econstructor; eauto.
 Qed.
 
 Lemma transl_Sassign_correct:
@@ -831,7 +818,7 @@ Lemma transl_Ssequence_1_correct:
         exec_stmt_prop e m (Ssequence s1 s2) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. 
+  red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. 
 Qed.
 
 Lemma transl_Ssequence_2_correct:
@@ -843,7 +830,7 @@ Lemma transl_Ssequence_2_correct:
         exec_stmt_prop e m (Ssequence s1 s2) t1 m1 out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. eapply exec_Sseq_stop; eauto. 
+  eapply exec_Sseq_stop; eauto. 
   destruct out; simpl; congruence.
 Qed.
 
@@ -860,7 +847,7 @@ Lemma transl_Sifthenelse_true_correct:
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
   exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]].
-  subst ts. eapply exec_Sifthenelse_true; eauto. 
+  eapply exec_Sifthenelse_true; eauto. 
 Qed.
 
 Lemma transl_Sifthenelse_false_correct:
@@ -876,7 +863,7 @@ Lemma transl_Sifthenelse_false_correct:
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
   exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]].
-  subst ts. eapply exec_Sifthenelse_false; eauto. 
+  eapply exec_Sifthenelse_false; eauto. 
 Qed.
 
 Lemma transl_Sreturn_none_correct:
@@ -884,7 +871,7 @@ Lemma transl_Sreturn_none_correct:
         exec_stmt_prop e m (Csyntax.Sreturn None) E0 m (Csem.Out_return None)).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl. apply exec_Sreturn_none. 
+  simpl. apply exec_Sreturn_none. 
 Qed.
 
 Lemma transl_Sreturn_some_correct:
@@ -896,7 +883,7 @@ Lemma transl_Sreturn_some_correct:
           (Csem.Out_return (Some v))).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl. eapply exec_Sreturn_some; eauto. 
+  simpl. eapply exec_Sreturn_some; eauto. 
 Qed.
 
 Lemma transl_Sbreak_correct:
@@ -904,7 +891,7 @@ Lemma transl_Sbreak_correct:
         exec_stmt_prop e m Sbreak E0 m Out_break).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl. apply exec_Sexit.  
+  simpl. apply exec_Sexit.  
 Qed.
 
 Lemma transl_Scontinue_correct:
@@ -912,19 +899,19 @@ Lemma transl_Scontinue_correct:
         exec_stmt_prop e m Scontinue E0 m Out_continue).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl. apply exec_Sexit.  
+  simpl. apply exec_Sexit.  
 Qed.
 
 Lemma exit_if_false_true:
   forall a ts e m1 t m2 v tyenv te,
-  exit_if_false a = Some ts ->
+  exit_if_false a = OK ts ->
   eval_expr_prop e m1 a t m2 v ->
   match_env tyenv e te ->
   wt_expr tyenv a ->
   is_true v (typeof a) ->
   exec_stmt tprog te m1 ts t m2 Out_normal.
 Proof.
-  intros. monadInv H. rewrite <- H5. 
+  intros. monadInv H. 
   exploit make_boolean_correct_true. eapply H0; eauto. eauto.
   intros [vb [EVAL ISTRUE]].
   eapply exec_Sifthenelse_true with (v1 := vb); eauto. 
@@ -933,14 +920,14 @@ Qed.
  
 Lemma exit_if_false_false:
   forall a ts e m1 t m2 v tyenv te,
-  exit_if_false a = Some ts ->
+  exit_if_false a = OK ts ->
   eval_expr_prop e m1 a t m2 v ->
   match_env tyenv e te ->
   wt_expr tyenv a ->
   is_false v (typeof a) ->
   exec_stmt tprog te m1 ts t m2 (Out_exit 0).
 Proof.
-  intros. monadInv H. rewrite <- H5. 
+  intros. monadInv H. 
   exploit make_boolean_correct_false. eapply H0; eauto. eauto.
   intros [vb [EVAL ISFALSE]].
   eapply exec_Sifthenelse_false with (v1 := vb); eauto. 
@@ -956,7 +943,7 @@ Lemma transl_Swhile_false_correct:
         exec_stmt_prop e m (Swhile a s) t m1 Csem.Out_normal).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl.
+  simpl.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. apply exec_Sseq_stop.
   eapply exit_if_false_false; eauto. congruence. congruence.
@@ -992,7 +979,7 @@ Lemma transl_Swhile_stop_correct:
         exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. rewrite (transl_out_break_or_return _ _ nbrk ncnt H4).
+  rewrite (transl_out_break_or_return _ _ nbrk ncnt H4).
   apply exec_Sblock. apply exec_Sloop_stop. 
   eapply exec_Sseq_continue. 
   eapply exit_if_false_true; eauto. 
@@ -1017,7 +1004,6 @@ Proof.
   intros; red; intros. 
   exploit H6; eauto. intro NEXTITER.
   inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. 
   inversion NEXTITER; subst.
   apply exec_Sblock. 
   eapply exec_Sloop_loop. eapply exec_Sseq_continue.
@@ -1041,7 +1027,7 @@ Lemma transl_Sdowhile_false_correct:
         exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 Csem.Out_normal).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl.
+  simpl.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue.
   rewrite (transl_out_normal_or_continue out1 H1).
@@ -1058,7 +1044,7 @@ Lemma transl_Sdowhile_stop_correct:
         exec_stmt_prop e m (Sdowhile a s) t m1 out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl.
+  simpl.
   assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal).
     inversion H1; simpl; congruence.
   rewrite (transl_out_break_or_return _ _ nbrk ncnt H1). 
@@ -1084,7 +1070,6 @@ Proof.
   intros; red; intros. 
   exploit H6; eauto. intro NEXTITER.
   inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. 
   inversion NEXTITER; subst.
   apply exec_Sblock. 
   eapply exec_Sloop_loop. eapply exec_Sseq_continue.
@@ -1129,7 +1114,7 @@ Lemma transl_Sfor_false_correct:
         exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 Csem.Out_normal).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl.
+  simpl.
   eapply exec_Sseq_continue. apply exec_Sskip.
   change Out_normal with (outcome_block (Out_exit 0)).
   apply exec_Sblock. apply exec_Sloop_stop. 
@@ -1150,7 +1135,7 @@ Lemma transl_Sfor_stop_correct:
         exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2) m2 out).
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. simpl.
+  simpl.
   assert (outcome_block (transl_outcome 1 0 out2) <> Out_normal).
     inversion H4; simpl; congruence.
   rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). 
@@ -1181,7 +1166,6 @@ Proof.
   intros; red; intros. 
   exploit H8; eauto. intro NEXTITER.
   inversion WT; clear WT; subst. simpl in TR; monadInv TR.
-  subst ts. 
   inversion NEXTITER; subst.
   inversion H11; subst.
   inversion H18; subst.   
@@ -1205,7 +1189,7 @@ Lemma transl_lblstmts_switch:
   transl_lblstmts 
     (lblstmts_length sl)
     (S (lblstmts_length sl + ncnt))
-    sl (Sblock body) = Some ts ->
+    sl (Sblock body) = OK ts ->
   wt_lblstmts tyenv sl ->
   match_env tyenv e te ->
   exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out ->
@@ -1226,7 +1210,7 @@ Proof.
   (* next case selected *)
   inversion H1; clear H1; subst.
   simpl in H0; monadInv H0.
-  eapply IHsl with (body := Sseq (Sblock body) s0); eauto.
+  eapply IHsl with (body := Sseq (Sblock body) x); eauto.
   apply exec_Sseq_stop. 
   change (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0)))
     with (outcome_block (Out_exit (S (switch_target n (lblstmts_length sl) (switch_table sl 0))))).
@@ -1247,7 +1231,7 @@ Lemma transl_Sswitch_correct:
 Proof.
   intros; red; intros.
   inversion WT; clear WT; subst.
-  simpl in TR. monadInv TR; clear TR. 
+  simpl in TR. monadInv TR. 
   rewrite length_switch_table in EQ0. 
   replace (ncnt + lblstmts_length sl + 1)%nat
      with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega.
@@ -1265,7 +1249,6 @@ Proof.
   intros; red; intros.
   inversion WT; subst.
   simpl in TR. monadInv TR.
-  rewrite <- H3. 
   replace (transl_outcome nbrk ncnt (outcome_switch out))
      with (outcome_block (transl_outcome 0 (S ncnt) out)).
   constructor. 
@@ -1286,8 +1269,8 @@ Lemma transl_LScase_fallthrough_correct:
 Proof.
   intros; red; intros.
   inversion WT; subst.
-  simpl in TR. monadInv TR; clear TR.
-  assert (exec_stmt tprog te m0 (Sblock (Sseq body s0)) 
+  monadInv TR.
+  assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) 
                   (t0 ** t1) m1 Out_normal).
   change Out_normal with
     (outcome_block (transl_outcome (S (lblstmts_length ls))
@@ -1311,19 +1294,19 @@ Lemma transl_LScase_stop_correct:
 Proof.
   intros; red; intros.
   inversion WT; subst.
-  simpl in TR. monadInv TR; clear TR.
+  monadInv TR.
   exploit H0; eauto. intro EXEC.
   destruct out; simpl; simpl in EXEC.
   (* out = Out_break *)
   change Out_normal with (outcome_block (Out_exit 0)).
-  eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto.
+  eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto.
   rewrite plus_0_r. 
   change (Out_exit (lblstmts_length ls))
     with (outcome_block (Out_exit (S (lblstmts_length ls)))).
   constructor. eapply exec_Sseq_continue; eauto.
   (* out = Out_continue *)
   change (Out_exit ncnt) with (outcome_block (Out_exit (S ncnt))).
-  eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto.
+  eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto.
   replace (Out_exit (lblstmts_length ls + S ncnt))
     with (outcome_block (Out_exit (S (S (lblstmts_length ls + ncnt))))).
   constructor. eapply exec_Sseq_continue; eauto.
@@ -1331,7 +1314,7 @@ Proof.
   (* out = Out_normal *)
   congruence.
   (* out = Out_return *)
-  eapply transl_lblstmts_return with (body := Sblock (Sseq body s0)); eauto.
+  eapply transl_lblstmts_return with (body := Sblock (Sseq body x)); eauto.
   change (Out_return o)
     with (outcome_block (Out_return o)).
   constructor. eapply exec_Sseq_continue; eauto.
@@ -1366,13 +1349,13 @@ Proof.
   inversion WT; clear WT; subst. 
   inversion H6; clear H6; subst.
   (* Exploitation of translation hypothesis *)
-  monadInv TR. subst tf. clear TR. 
-  monadInv EQ. clear EQ. subst f0.
+  monadInv TR. 
+  monadInv EQ.
   (* Allocation of variables *)
   exploit match_env_alloc_variables; eauto.
   apply match_globalenv_match_env_empty. 
   apply match_global_typenv.
-  eexact (transl_fn_variables _ _ (signature_of_function f) _ _ s EQ0 EQ1).
+  eexact (transl_fn_variables _ _ (signature_of_function f) _ _ x2 EQ0 EQ).
   intros [te [ALLOCVARS MATCHENV]].
   (* Execution *)
   econstructor; simpl.
@@ -1395,7 +1378,7 @@ Lemma transl_funcall_external_correct:
         eval_funcall_prop m (External id targs tres) vargs t m vres).
 Proof.
   intros; red; intros.
-  monadInv TR. subst tf. constructor. auto.
+  monadInv TR. constructor. auto.
 Qed.
 
 Theorem transl_funcall_correct:
@@ -1467,7 +1450,7 @@ End CORRECTNESS.
 
 Theorem transl_program_correct:
   forall prog tprog t r,
-  transl_program prog = Some tprog ->
+  transl_program prog = OK tprog ->
   Ctyping.wt_program prog ->
   Csem.exec_program prog t r ->
   Csharpminor.exec_program tprog t r.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index f9463e65..6a5fcf34 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -1,6 +1,7 @@
 (** * Abstract syntax for the Clight language *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Integers.
 Require Import Floats.
 Require Import AST.
@@ -251,17 +252,19 @@ Qed.
 
 (** Byte offset for a field in a struct. *)
 
+Open Local Scope string_scope.
+
 Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
-                              {struct fld} : option Z :=
+                              {struct fld} : res Z :=
   match fld with
-  | Fnil => None
+  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
   | Fcons id' t fld' =>
       if ident_eq id id'
-      then Some (align pos (alignof t))
+      then OK (align pos (alignof t))
       else field_offset_rec id fld' (align pos (alignof t) + sizeof t)
   end.
 
-Definition field_offset (id: ident) (fld: fieldlist) : option Z :=
+Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
   field_offset_rec id fld 0.
 
 (* Describe how a variable of the given type must be accessed: