Ported to Coq 8.4pl1. Merge of branches/coq-8.4.

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

12 files changed, 454 insertions, 436 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d425693..3830ca7 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -125,16 +125,12 @@ let name_for_string_literal env s =
     id
 
 let typeStringLiteral s =
-  Tarray(Tint(I8, Unsigned, noattr),
-         z_of_camlint(Int32.of_int(String.length s + 1)),
-         noattr)
+  Tarray(Tint(I8, Unsigned, noattr), Z.of_uint (String.length s + 1), noattr)
 
 let global_for_string s id =
   let init = ref [] in
   let add_char c =
-    init :=
-       AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c)))
-       :: !init in
+    init := AST.Init_int8(Z.of_uint(Char.code c)) :: !init in
   add_char '\000';
   for i = String.length s - 1 downto 0 do add_char s.[i] done;
   (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init;
@@ -344,8 +340,8 @@ let supported_return_type env ty =
 (** Floating point constants *)
 
 let z_of_str hex str fst =
-  let res = ref BinInt.Z0 in
-  let base = if hex then 16l else 10l in
+  let res = ref Z.Z0 in
+  let base = if hex then 16 else 10 in
   for i = fst to String.length str - 1 do
     let d = int_of_char str.[i] in
     let d =
@@ -356,27 +352,25 @@ let z_of_str hex str fst =
       else
 	d - int_of_char '0'
     in
-    let d = Int32.of_int d in
-    assert (d >= 0l && d < base);
-    res := BinInt.coq_Zplus
-      (BinInt.coq_Zmult (z_of_camlint base) !res) (z_of_camlint d)
+    assert (d >= 0 && d < base);
+    res := Z.add (Z.mul (Z.of_uint base) !res) (Z.of_uint d)
   done;
   !res
 
 let convertFloat f kind =
   let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in
   match mant with
-    | BinInt.Z0 -> Float.zero
-    | BinInt.Zpos mant ->
+    | Z.Z0 -> Float.zero
+    | Z.Zpos mant ->
 
       let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in
       let exp = z_of_str false f.C.exp (if sgExp then 1 else 0) in
-      let exp = if f.C.exp.[0] = '-' then BinInt.coq_Zopp exp else exp in
+      let exp = if f.C.exp.[0] = '-' then Z.neg exp else exp in
       let shift_exp =
-	Int32.of_int ((if f.C.hex then 4 else 1) * String.length f.C.fracPart) in
-      let exp = BinInt.coq_Zminus exp (z_of_camlint shift_exp) in
+	(if f.C.hex then 4 else 1) * String.length f.C.fracPart in
+      let exp = Z.sub exp (Z.of_uint shift_exp) in
 
-      let base = positive_of_camlint (if f.C.hex then 16l else 10l) in
+      let base = P.of_int (if f.C.hex then 16 else 10) in
 
       begin match kind with
 	| FFloat ->
@@ -384,7 +378,8 @@ let convertFloat f kind =
 	| FDouble | FLongDouble ->
 	  Float.build_from_parsed64 base mant exp
       end
-    | BinInt.Zneg _ -> assert false
+
+    | Z.Zneg _ -> assert false
 
 (** Expressions *)
 
@@ -752,7 +747,7 @@ let string_of_errmsg msg =
   let string_of_err = function
   | Errors.MSG s -> camlstring_of_coqstring s
   | Errors.CTX i -> extern_atom i
-  | Errors.POS i -> sprintf "%ld" (camlint_of_positive i)
+  | Errors.POS i -> Z.to_string (Z.Zpos i)
   in String.concat "" (List.map string_of_err msg)
 
 let rec convertInit env init =
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index c370c60..ded6b72 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -132,7 +132,7 @@ Proof.
   intros. destruct v; destruct t; simpl in H; inv H.
   constructor.
   constructor.
-  destruct (Genv.invert_symbol ge b) as [id|]_eqn; inv H1. 
+  destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. 
   constructor. apply Genv.invert_find_symbol; auto.
 Qed.
 
@@ -148,8 +148,8 @@ Lemma list_eventval_of_val_sound:
 Proof with try discriminate.
   induction vl; destruct tl; simpl; intros; inv H.
   constructor.
-  destruct (eventval_of_val a t) as [ev1|]_eqn...
-  destruct (list_eventval_of_val vl tl) as [evl'|]_eqn...
+  destruct (eventval_of_val a t) as [ev1|] eqn:?...
+  destruct (list_eventval_of_val vl tl) as [evl'|] eqn:?...
   inv H1. constructor. apply eventval_of_val_sound; auto. eauto.
 Qed.
 
@@ -166,7 +166,7 @@ Proof.
   intros. destruct ev; destruct t; simpl in H; inv H.
   constructor.
   constructor.
-  destruct (Genv.find_symbol ge i) as [b|]_eqn; inv H1.
+  destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
   constructor. auto.
 Qed.
 
@@ -207,8 +207,8 @@ Ltac mydestr :=
   match goal with
   | [ |- None = Some _ -> _ ] => intro X; discriminate
   | [ |- Some _ = Some _ -> _ ] => intro X; inv X
-  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
-  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
+  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
+  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
   | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
   | _ => idtac
   end.
@@ -331,7 +331,7 @@ Lemma do_deref_loc_sound:
   deref_loc ge ty m b ofs t v /\ possible_trace w t w'.
 Proof.
   unfold do_deref_loc; intros until v.
-  destruct (access_mode ty) as []_eqn; mydestr. 
+  destruct (access_mode ty) eqn:?; mydestr. 
   intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. 
   split. eapply deref_loc_value; eauto. constructor.
   split. eapply deref_loc_reference; eauto. constructor.
@@ -356,7 +356,7 @@ Lemma do_assign_loc_sound:
   assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'.
 Proof.
   unfold do_assign_loc; intros until m'.
-  destruct (access_mode ty) as []_eqn; mydestr. 
+  destruct (access_mode ty) eqn:?; mydestr. 
   intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. 
   split. eapply assign_loc_value; eauto. constructor.
   destruct v; mydestr. destruct a as [P [Q R]]. 
@@ -558,7 +558,7 @@ Proof with try congruence.
   intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto.
 (* EF_malloc *)
   unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
-  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr.
+  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr.
   split. econstructor; eauto. constructor.
 (* EF_free *)
   unfold do_ef_free. destruct vargs... destruct v... destruct vargs... 
@@ -1170,7 +1170,7 @@ Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop
 Ltac monadInv :=
   match goal with
   | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] =>
-      destruct x as []_eqn; [monadInv|discriminate]
+      destruct x eqn:?; [monadInv|discriminate]
   | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] =>
       destruct x; [monadInv|discriminate]
   | _ => idtac
@@ -1338,8 +1338,8 @@ Lemma is_val_list_all_values:
   forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al.
 Proof.
   induction al; simpl; intros. auto. 
-  destruct (is_val r1) as [[v ty]|]_eqn; try discriminate.
-  destruct (is_val_list al) as [vtl'|]_eqn; try discriminate.
+  destruct (is_val r1) as [[v ty]|] eqn:?; try discriminate.
+  destruct (is_val_list al) as [vtl'|] eqn:?; try discriminate.
   rewrite (is_val_inv _ _ _ Heqo). eauto.
 Qed.
 
@@ -1360,91 +1360,91 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* Eval *)
   split; intros. tauto. simpl; congruence.
 (* Evar *)
-  destruct (e!x) as [[b ty']|]_eqn.
+  destruct (e!x) as [[b ty']|] eqn:?.
   destruct (type_eq ty ty')...
   subst. apply topred_ok; auto. apply red_var_local; auto.
-  destruct (Genv.find_symbol ge x) as [b|]_eqn...
-  destruct (type_of_global ge b) as [ty'|]_eqn...
+  destruct (Genv.find_symbol ge x) as [b|] eqn:?...
+  destruct (type_of_global ge b) as [ty'|] eqn:?...
   destruct (type_eq ty ty')...
   subst. apply topred_ok; auto. apply red_var_global; auto.
 (* Efield *)
-  destruct (is_val a) as [[v ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo).
   destruct v...
   destruct ty'... 
   (* top struct *)
-  destruct (field_offset f f0) as [delta|]_eqn...
+  destruct (field_offset f f0) as [delta|] eqn:?...
   apply topred_ok; auto. apply red_field_struct; auto.
   (* top union *)
   apply topred_ok; auto. apply red_field_union; auto.
   (* in depth *)
   eapply incontext_ok; eauto. 
 (* Evalof *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo).
+  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
   destruct (type_eq ty ty')... subst ty'.
-  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
   exploit do_deref_loc_sound; eauto. intros [A B].
   apply topred_ok; auto. red. split. apply red_rvalof; auto. exists w'; auto.
   apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext_ok; eauto.
 (* Ederef *)
-  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo).
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
   destruct v... apply topred_ok; auto. apply red_deref; auto. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* Eaddrof *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo).
+  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
   apply topred_ok; auto. split. apply red_addrof; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* unop *)
-  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (sem_unary_operation op v ty') as [v'|]_eqn...
+  destruct (sem_unary_operation op v ty') as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* binop *)
-  destruct (is_val a1) as [[v1 ty1] | ]_eqn. 
-  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  destruct (is_val a1) as [[v1 ty1] | ] eqn:?. 
+  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
   (* top *)
-  destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|]_eqn...
+  destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|] eqn:?...
   apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor.
   (* depth *)
   eapply incontext2_ok; eauto. 
   eapply incontext2_ok; eauto. 
 (* cast *)
-  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (sem_cast v ty' ty) as [v'|]_eqn...
+  destruct (sem_cast v ty' ty) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* seqand *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (bool_val v ty') as [v'|]_eqn... destruct v'.
+  destruct (bool_val v ty') as [v'|] eqn:?... destruct v'.
   apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor.
   apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* seqor *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (bool_val v ty') as [v'|]_eqn... destruct v'.
+  destruct (bool_val v ty') as [v'|] eqn:?... destruct v'.
   apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor.
   apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* condition *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (bool_val v ty') as [v'|]_eqn...
+  destruct (bool_val v ty') as [v'|] eqn:?...
   apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1453,13 +1453,13 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* alignof *)
   apply topred_ok; auto. split. apply red_alignof. exists w; constructor.
 (* assign *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
-  destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
+  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. 
+  destruct (is_val a2) as [[v2 ty2] | ] eqn:?. 
   rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
-  destruct (sem_cast v2 ty2 ty) as [v|]_eqn...
-  destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|]_eqn.
+  destruct (sem_cast v2 ty2 ty) as [v|] eqn:?...
+  destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?.
   exploit do_assign_loc_sound; eauto. intros [P Q].
   apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto.
   apply not_invert_ok; simpl; intros; myinv. exploit do_assign_loc_complete; eauto. congruence.
@@ -1467,12 +1467,12 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* assignop *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
-  destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
+  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. 
+  destruct (is_val a2) as [[v2 ty2] | ] eqn:?. 
   rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
   (* top *)
   destruct (type_eq ty1 ty)... subst ty1.
-  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
   exploit do_deref_loc_sound; eauto. intros [A B].
   apply topred_ok; auto. red. split. apply red_assignop; auto. exists w'; auto.
   apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
@@ -1480,30 +1480,30 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* postincr *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo). 
+  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). 
   (* top *)
   destruct (type_eq ty' ty)... subst ty'.
-  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
   exploit do_deref_loc_sound; eauto. intros [A B].
   apply topred_ok; auto. red. split. apply red_postincr; auto. exists w'; auto.
   apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext_ok; eauto.
 (* comma *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
   destruct (type_eq (typeof a2) ty)... subst ty.
   apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* call *)
-  destruct (is_val a) as [[vf tyf] | ]_eqn.  
-  destruct (is_val_list rargs) as [vtl | ]_eqn. 
+  destruct (is_val a) as [[vf tyf] | ] eqn:?.  
+  destruct (is_val_list rargs) as [vtl | ] eqn:?. 
   rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (classify_fun tyf) as [tyargs tyres|]_eqn...
-  destruct (Genv.find_funct ge vf) as [fd|]_eqn...
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... 
+  destruct (classify_fun tyf) as [tyargs tyres|] eqn:?...
+  destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
+  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
   destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))...
   apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. 
   eapply sem_cast_arguments_sound; eauto.
@@ -1516,11 +1516,11 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext2_list_ok; eauto.
   eapply incontext2_list_ok; eauto.
 (* builtin *)
-  destruct (is_val_list rargs) as [vtl | ]_eqn. 
+  destruct (is_val_list rargs) as [vtl | ] eqn:?. 
   exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... 
-  destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ]_eqn...
+  destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
+  destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?...
   exploit do_ef_external_sound; eauto. intros [EC PT].
   apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. 
   eapply sem_cast_arguments_sound; eauto.
@@ -1537,9 +1537,9 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
 (* loc *)
   split; intros. tauto. simpl; congruence.
 (* paren *)
-  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
+  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  destruct (sem_cast v ty' ty) as [v'|]_eqn...
+  destruct (sem_cast v ty' ty) as [v'|] eqn:?...
   apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
@@ -1556,8 +1556,8 @@ Lemma step_exprlist_val_list:
 Proof.
   induction al; simpl; intros. 
   auto.
-  destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence.
-  destruct (is_val_list al) as []_eqn; try congruence.
+  destruct (is_val r1) as [[v1 ty1]|] eqn:?; try congruence.
+  destruct (is_val_list al) eqn:?; try congruence.
   rewrite (is_val_inv _ _ _ Heqo).
   rewrite IHal. auto. congruence.
 Qed.
@@ -1717,75 +1717,78 @@ with step_exprlist_context:
 Proof.
   induction 1; simpl; intros.
 (* top *)
-  red. destruct (step_expr k a m); auto. intros. 
-  replace (fun x => C1 x) with C1; auto. apply extensionality; auto.
+  red. destruct (step_expr k a m); auto.
+  try (* no eta in 8.3 *)
+   (intros;
+    replace (fun x => C1 x) with C1 by (apply extensionality; auto);
+    auto).
 (* deref *)
   eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* field *)
   eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* valof *)
   eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
 (* addrof *)
   eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
 (* unop *)
   eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* binop left *)
   eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* binop right *)
   eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto.
-  destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto.
-  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+  destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
 (* cast *)
   eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* seqand *)
   eapply reducts_incl_trans with (C' := fun x => Eseqand x r2 ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* seqor *)
   eapply reducts_incl_trans with (C' := fun x => Eseqor x r2 ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* condition *)
   eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* assign left *)
   eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
 (* assign right *)
   eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto.
-  destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto.
-  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+  destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
 (* assignop left *)
   eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
 (* assignop right *)
   eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto.
-  destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto.
-  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+  destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
 (* postincr *)
   eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
 (* call left *)
   eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* call right *)
   eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. 
-  destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto.
-  destruct (is_val_list (C a)) as [vl|]_eqn; eauto.
+  destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto.
+  destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
 (* builtin *)
   eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto. 
-  destruct (is_val_list (C a)) as [vl|]_eqn; eauto.
+  destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
 (* comma *)
   eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 (* paren *)
   eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto.
-  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
 
   induction 1; simpl; intros.
 (* cons left *)
@@ -1804,7 +1807,7 @@ Lemma not_stuckred_imm_safe:
   (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m.
 Proof.
   intros. generalize (step_expr_sound a k m). intros [A B]. 
-  destruct (step_expr k a m) as [|[C rd] res]_eqn.
+  destruct (step_expr k a m) as [|[C rd] res] eqn:?.
   specialize (B (refl_equal _)). destruct k.
   destruct a; simpl in B; try congruence. constructor.
   destruct a; simpl in B; try congruence. constructor.
@@ -1889,7 +1892,7 @@ Lemma do_alloc_variables_sound:
 Proof.
   induction l; intros; simpl. 
   constructor.
-  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1]_eqn; simpl.
+  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1] eqn:?; simpl.
   econstructor; eauto.
 Qed.
 
@@ -2053,8 +2056,8 @@ Ltac myinv :=
         [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
   | [ |- In _ (_ :: nil) -> _ ] => 
         intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
-  | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x as []_eqn; myinv
-  | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x as []_eqn; myinv
+  | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
+  | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
   | _ => idtac
   end.
@@ -2078,7 +2081,7 @@ Proof with try (left; right; econstructor; eauto; fail).
   (* goto *)
   destruct p as [s' k']. myinv...
 (* ExprState *)
-  destruct (is_val r) as [[v ty]|]_eqn.
+  destruct (is_val r) as [[v ty]|] eqn:?.
   (* expression is a value *)
   rewrite (is_val_inv _ _ _ Heqo).
   destruct k; myinv...
@@ -2102,7 +2105,7 @@ Proof with try (left; right; econstructor; eauto; fail).
 (* callstate *)
   destruct fd; myinv.
   (* internal *)
-  destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn.
+  destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1] eqn:?.
   myinv. left; right; apply step_internal_function with m1. auto. 
   change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. 
   apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 62690d6..cff5b06 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -398,11 +398,11 @@ Proof.
                                else false
                       end
                  end).
-  destruct (List.existsb pred (PTree.elements e)) as []_eqn.
+  destruct (List.existsb pred (PTree.elements e)) eqn:?.
   (* yes *)
   rewrite List.existsb_exists in Heqb. 
   destruct Heqb as [[id [b sz]] [A B]].
-  simpl in B. destruct (f b) as [[sp' delta] |]_eqn; try discriminate.
+  simpl in B. destruct (f b) as [[sp' delta] |] eqn:?; try discriminate.
   destruct (eq_block sp sp'); try discriminate.
   destruct (andb_prop _ _ B).
   left. apply is_reachable_intro with id b sz delta.
@@ -646,13 +646,13 @@ Proof.
   constructor. auto. auto. 
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto. 
-  red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|]_eqn. 
+  red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?. 
   exploit INCR; eauto. congruence.
   exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. 
   intros. assert (lo <= hi) by (eapply me_low_high; eauto).
-  destruct (f1 b) as [[b' delta']|]_eqn. 
+  destruct (f1 b) as [[b' delta']|] eqn:?. 
   apply INCR; auto. 
-  destruct (f2 b) as [[b' delta']|]_eqn; auto.
+  destruct (f2 b) as [[b' delta']|] eqn:?; auto.
   exploit SEPARATED; eauto. intros [A B]. elim A. red. omega.
   eapply match_bounds_invariant; eauto. 
   intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. omega. 
@@ -884,7 +884,7 @@ Proof.
   intros. destruct (In_dec peq id (map fst vars)).
   apply cenv_remove_gss; auto.
   rewrite cenv_remove_gso; auto.
-  destruct (cenv!id) as [ofs|]_eqn; auto. elim n; eauto. 
+  destruct (cenv!id) as [ofs|] eqn:?; auto. elim n; eauto. 
   eapply Mem.alloc_right_inject; eauto. 
 Qed.
 
@@ -917,7 +917,7 @@ Proof.
   simpl; intros. inv H. omega.
 Opaque assign_variable.
   destruct a as [id s]. simpl. intros.
-  destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1]_eqn. 
+  destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. 
   apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto.
 Transparent assign_variable.
 Qed.
@@ -1014,7 +1014,7 @@ Proof.
   destruct a as [id sz].
   simpl in H0. inv H0. rewrite in_app in H6.
   rewrite list_norepet_app in H7. destruct H7 as [P [Q R]].
-  destruct (assign_variable (cenv1, sz1) (id, sz)) as [cenv' sz']_eqn.
+  destruct (assign_variable (cenv1, sz1) (id, sz)) as [cenv' sz'] eqn:?.
   exploit assign_variable_sound.
     eauto.
     instantiate (1 := vars). tauto.
@@ -1377,12 +1377,12 @@ Proof.
     intros. apply (val_match_approx_increasing Int1 a v); auto.
 
   intros; unfold Approx.bitwise_and. 
-  destruct (Approx.bge Int1 a1) as []_eqn. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int1 a2) as []_eqn. simpl. apply X; eauto. compute; auto.
-  destruct (Approx.bge Int8u a1) as []_eqn. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int8u a2) as []_eqn. simpl. apply X; eauto. compute; auto.
-  destruct (Approx.bge Int16u a1) as []_eqn. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int16u a2) as []_eqn. simpl. apply X; eauto. compute; auto.
+  destruct (Approx.bge Int1 a1) eqn:?. simpl. apply Y; eauto. compute; auto.
+  destruct (Approx.bge Int1 a2) eqn:?. simpl. apply X; eauto. compute; auto.
+  destruct (Approx.bge Int8u a1) eqn:?. simpl. apply Y; eauto. compute; auto.
+  destruct (Approx.bge Int8u a2) eqn:?. simpl. apply X; eauto. compute; auto.
+  destruct (Approx.bge Int16u a1) eqn:?. simpl. apply Y; eauto. compute; auto.
+  destruct (Approx.bge Int16u a2) eqn:?. simpl. apply X; eauto. compute; auto.
   simpl; auto. 
 Qed.
 
@@ -1404,19 +1404,19 @@ Proof.
 
   unfold Approx.bitwise_or. 
 
-  destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) as []_eqn.
+  destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) eqn:?.
   destruct (andb_prop _ _ Heqb).
   simpl. apply X. compute; auto. 
   apply (val_match_approx_increasing Int1 a1 v1); auto.
   apply (val_match_approx_increasing Int1 a2 v2); auto.
 
-  destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) as []_eqn.
+  destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   simpl. apply X. compute; auto. 
   apply (val_match_approx_increasing Int8u a1 v1); auto.
   apply (val_match_approx_increasing Int8u a2 v2); auto.
 
-  destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) as []_eqn.
+  destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) eqn:?.
   destruct (andb_prop _ _ Heqb1).
   simpl. apply X. compute; auto. 
   apply (val_match_approx_increasing Int16u a1 v1); auto.
@@ -1574,8 +1574,8 @@ Proof.
     apply val_inject_val_of_optbool.
 Opaque Int.add.
     unfold Val.cmpu. simpl. 
-    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; simpl; auto.
-    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; simpl; auto.
+    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto.
+    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto.
     exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. 
     intros V1. rewrite V1.
     exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
@@ -1859,13 +1859,20 @@ Proof.
     (forall b ofs, Mem.store chunk m1 b ofs v1 = Mem.store chunk m1 b ofs v1') ->
     Mem.storev chunk m1 a1 v1' = Some n1).
   intros. rewrite <- H0. destruct a1; simpl; auto. 
-  inv H2; (eapply Mem.storev_mapped_inject; [eauto|idtac|eauto|eauto]);
-  auto; apply H3; intros.
+  inv H2; eapply Mem.storev_mapped_inject;
+  try eapply H; try eapply H1; try apply H3; intros.
   rewrite <- Mem.store_int8_sign_ext. rewrite H4. apply Mem.store_int8_sign_ext.
+  auto.
   rewrite <- Mem.store_int8_zero_ext. rewrite H4. apply Mem.store_int8_zero_ext.
+  auto.
   rewrite <- Mem.store_int16_sign_ext. rewrite H4. apply Mem.store_int16_sign_ext.
+  auto.
   rewrite <- Mem.store_int16_zero_ext. rewrite H4. apply Mem.store_int16_zero_ext.
+  auto.
   rewrite <- Mem.store_float32_truncate. rewrite H4. apply Mem.store_float32_truncate.
+  auto.
+  eauto.
+  auto.
 Qed.
 
 Lemma make_store_correct:
@@ -2053,7 +2060,7 @@ Proof.
   (* Eunop *)
   exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
   unfold Csharpminor.eval_unop in H0. 
-  destruct (Approx.unop_is_redundant op x0) as []_eqn; inv EQ0.
+  destruct (Approx.unop_is_redundant op x0) eqn:?; inv EQ0.
   (* -- eliminated *)
   exploit approx_unop_is_redundant_sound; eauto. intros. 
   replace v with v1 by congruence.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 42eae5d..74a6da5 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -732,10 +732,10 @@ Lemma block_is_volatile_preserved:
   forall b, block_is_volatile tge b = block_is_volatile ge b.
 Proof.
   intros. unfold block_is_volatile.
-  destruct (Genv.find_var_info ge b) as []_eqn.
+  destruct (Genv.find_var_info ge b) eqn:?.
   exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. 
   unfold transf_globvar in B. monadInv B. auto.
-  destruct (Genv.find_var_info tge b) as []_eqn.
+  destruct (Genv.find_var_info tge b) eqn:?.
   exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence.
   auto.
 Qed.
@@ -761,7 +761,7 @@ Lemma match_env_globals:
   e!id = None ->
   te!id = None.
 Proof.
-  intros. destruct (te!id) as [[b sz] | ]_eqn; auto.
+  intros. destruct (te!id) as [[b sz] | ] eqn:?; auto.
   exploit me_local_inv; eauto. intros [ty EQ]. congruence.
 Qed.
 
@@ -1284,7 +1284,7 @@ Proof.
   destruct H0. inv MK.
   econstructor; split.
   eapply plus_left.
-  destruct H0; subst ts'; constructor. 
+  destruct H0; subst ts'. 2:constructor. constructor.
   apply star_one. constructor. traceEq.
   econstructor; eauto. constructor. econstructor; eauto. 
 
@@ -1355,7 +1355,7 @@ Proof.
     destruct H; subst x; monadInv TR; inv MTR; auto.
   destruct H0. inv MK.
   econstructor; split.
-  apply plus_one. destruct H0; subst ts'; constructor.
+  apply plus_one. destruct H0; subst ts'. 2:constructor. constructor.
   eapply match_states_skip; eauto.
 
 
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b28409d..7988dfa 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -816,7 +816,7 @@ Ltac StepR REC C' a :=
 (* field *)
   StepR IHa (fun x => C(Efield x f0 ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl.
-  intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) as []_eqn; try contradiction.
+  intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction.
   destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
   exists b; exists ofs; econstructor; eauto.
 (* valof *)
@@ -1075,7 +1075,7 @@ Ltac Base :=
   Kind. Rec H RV C (fun x => Efield x f0 ty).
 (* rvalof *)
   Kind. Rec H LV C (fun x => Evalof x ty).
-  destruct (type_is_volatile (typeof l)) as []_eqn.
+  destruct (type_is_volatile (typeof l)) eqn:?.
   Base. rewrite H2; auto.
 (* deref *)
   Kind. Rec H RV C (fun x => Ederef x ty).
@@ -1198,7 +1198,7 @@ Proof.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
-  destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|]_eqn.
+  destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?.
   eapply star_left.
   left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto.  
   apply star_one. 
@@ -1326,8 +1326,8 @@ Proof.
   exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
-  destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|]_eqn.
-  destruct (sem_cast v3 tyres (typeof b1)) as [v4|]_eqn.
+  destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
+  destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
   destruct H2 as [t2 [m' D]].
   econstructor; econstructor; eapply step_assignop; eauto.
@@ -1341,8 +1341,8 @@ Proof.
   exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto.
   intros [b1 [ofs [E1 S1]]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
-  destruct (sem_incrdecr id v1 ty) as [v2|]_eqn.
-  destruct (sem_cast v2 (typeconv ty) ty) as [v3|]_eqn.
+  destruct (sem_incrdecr id v1 ty) as [v2|] eqn:?.
+  destruct (sem_cast v2 (typeconv ty) ty) as [v3|] eqn:?.
   destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')).
   destruct H0 as [t2 [m' D]].
   econstructor; econstructor; eapply step_postincr; eauto.
@@ -1493,8 +1493,8 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn.
+  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]]. 
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. 
@@ -1506,8 +1506,8 @@ Proof.
   rewrite Heqo; auto.
   (* assignop stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn.
-  destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn.
+  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
+  destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
   destruct H1 as [t2' [m'' P]]. 
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. 
@@ -1522,8 +1522,8 @@ Proof.
   subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
   econstructor; econstructor; eauto.
   inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
-  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn.
-  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn.
+  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]]. 
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. 
@@ -1535,8 +1535,8 @@ Proof.
   rewrite Heqo; auto.
   (* postincr stuck *)
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
-  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn.
-  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn.
+  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?.
+  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|] eqn:?.
   destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
   destruct H1 as [t2' [m'' P]]. 
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. 
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 9bc1dd7..ca9c5b0 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -12,7 +12,6 @@
 
 (** Compile-time evaluation of initializers for global C variables. *)
 
-Require Import Coq.Program.Equality.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
@@ -268,42 +267,58 @@ Proof.
   induction 2; simpl; try tauto. 
 Qed.
 
+Lemma compat_eval_steps_aux f r e m r' m' s2 :
+  simple r ->
+  star step ge s2 nil (ExprState f r' Kstop e m') ->
+  estep ge (ExprState f r Kstop e m) nil s2 ->
+  exists r1,
+    s2 = ExprState f r1 Kstop e m /\
+    compat_eval RV e r r1 m /\ simple r1.
+Proof.
+  intros.
+  inv H1.
+  (* lred *)
+  assert (S: simple a) by (eapply simple_context_1; eauto).
+  exploit lred_compat; eauto. intros [A B]. subst m'0.
+  econstructor; split. eauto. split.
+  eapply compat_eval_context; eauto.
+  eapply simple_context_2; eauto. eapply lred_simple; eauto.
+  (* rred *)
+  assert (S: simple a) by (eapply simple_context_1; eauto).
+  exploit rred_compat; eauto. intros [A B]. subst m'0.
+  econstructor; split. eauto. split.
+  eapply compat_eval_context; eauto.
+  eapply simple_context_2; eauto. eapply rred_simple; eauto.
+  (* callred *)
+  assert (S: simple a) by (eapply simple_context_1; eauto).
+  inv H8; simpl in S; contradiction.
+  (* stuckred *)
+  inv H0. destruct H1; inv H0.
+Qed.
+
 Lemma compat_eval_steps:
   forall f r e m  r' m',
   star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') ->
   simple r -> 
   m' = m /\ compat_eval RV e r r' m.
 Proof.
-  intros. dependent induction H.
+  intros. 
+  remember (ExprState f r Kstop e m) as S1.
+  remember E0 as t.
+  remember (ExprState f r' Kstop e m') as S2.
+  revert S1 t S2 H r m r' m' HeqS1 Heqt HeqS2 H0.
+  induction 1; intros; subst.
   (* base case *) 
-  split. auto. red; auto.
+  inv HeqS2. split. auto. red; auto.
   (* inductive case *)
   destruct (app_eq_nil t1 t2); auto. subst. inv H.
   (* expression step *)
-  assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1).
-    inv H3.
-    (* lred *)
-    assert (S: simple a) by (eapply simple_context_1; eauto).
-    exploit lred_compat; eauto. intros [A B]. subst m'0.
-    econstructor; split. eauto. split.
-    eapply compat_eval_context; eauto.
-    eapply simple_context_2; eauto. eapply lred_simple; eauto.
-    (* rred *)
-    assert (S: simple a) by (eapply simple_context_1; eauto).
-    exploit rred_compat; eauto. intros [A B]. subst m'0.
-    econstructor; split. eauto. split.
-    eapply compat_eval_context; eauto.
-    eapply simple_context_2; eauto. eapply rred_simple; eauto.
-    (* callred *)
-    assert (S: simple a) by (eapply simple_context_1; eauto).
-    inv H9; simpl in S; contradiction.
-    (* stuckred *)
-    inv H2. destruct H; inv H. 
-  destruct X as [r1 [A [B C]]]. subst s2. 
-  exploit IHstar; eauto. intros [D E]. 
+  exploit compat_eval_steps_aux; eauto.
+  intros [r1 [A [B C]]]. subst s2.
+  exploit IHstar; eauto. intros [D E].
   split. auto. destruct B; destruct E. split. congruence. auto. 
   (* statement steps *)
-  inv H3.
+  inv H1.
 Qed.
 
 Theorem eval_simple_steps:
@@ -438,7 +453,7 @@ Lemma sem_cast_match:
   forall v1' v2',  match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' ->
   match_val v2' v2.
 Proof.
-  intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] _eqn; inv H1.
+  intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:?; inv H1.
   unfold sem_cast in H; functional inversion Heqo; subst. 
   rewrite H2 in H. inv H0. inv H. constructor.
   rewrite H2 in H. inv H0. inv H. constructor; auto.
@@ -888,3 +903,4 @@ Qed.
 
 End SOUNDNESS.
 
+
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0e8b494..b05876a 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -40,8 +40,7 @@ let register_struct_union id fld =
 
 (* Naming temporaries *)
 
-let temp_name (id: ident) =
-  Printf.sprintf "$%ld" (camlint_of_positive id)
+let temp_name (id: ident) = Z.to_string (Z.Zpos id)
 
 (* Declarator (identifier + type) -- reuse from PrintCsyntax *)
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 7858545..67efd1b 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -396,7 +396,7 @@ let string_of_init id =
 
 let chop_last_nul id =
   match List.rev id with
-  | Init_int8 BinInt.Z0 :: tl -> List.rev tl
+  | Init_int8 Z.Z0 :: tl -> List.rev tl
   | _ -> id
 
 let print_init p = function
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index ab35445..2dbd97e 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -24,8 +24,6 @@ Require Import Cop.
 Require Import Csyntax.
 Require Import Clight.
 
-Module C := Csyntax.
-
 Open Local Scope string_scope.
 
 (** State and error monad for generating fresh identifiers. *)
@@ -208,46 +206,46 @@ Definition finish (dst: destination) (sl: list statement) (a: expr) :=
   | For_set tyl tmp => (sl ++ do_set tmp tyl a, a)
   end.
 
-Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr) :=
+Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
   match a with
-  | C.Eloc b ofs ty =>
-      error (msg "SimplExpr.transl_expr: C.Eloc")
-  | C.Evar x ty =>
+  | Csyntax.Eloc b ofs ty =>
+      error (msg "SimplExpr.transl_expr: Eloc")
+  | Csyntax.Evar x ty =>
       ret (finish dst nil (Evar x ty))
-  | C.Ederef r ty =>
+  | Csyntax.Ederef r ty =>
       do (sl, a) <- transl_expr For_val r;
       ret (finish dst sl (Ederef a ty))
-  | C.Efield r f ty =>
+  | Csyntax.Efield r f ty =>
       do (sl, a) <- transl_expr For_val r;
       ret (finish dst sl (Efield a f ty))
-  | C.Eval (Vint n) ty =>
+  | Csyntax.Eval (Vint n) ty =>
       ret (finish dst nil (Econst_int n ty))
-  | C.Eval (Vfloat n) ty =>
+  | Csyntax.Eval (Vfloat n) ty =>
       ret (finish dst nil (Econst_float n ty))
-  | C.Eval _ ty =>
-      error (msg "SimplExpr.transl_expr: val")
-  | C.Esizeof ty' ty =>
+  | Csyntax.Eval _ ty =>
+      error (msg "SimplExpr.transl_expr: Eval")
+  | Csyntax.Esizeof ty' ty =>
       ret (finish dst nil (Esizeof ty' ty))
-  | C.Ealignof ty' ty =>
+  | Csyntax.Ealignof ty' ty =>
       ret (finish dst nil (Ealignof ty' ty))
-  | C.Evalof l ty =>
+  | Csyntax.Evalof l ty =>
       do (sl1, a1) <- transl_expr For_val l;
-      do (sl2, a2) <- transl_valof (C.typeof l) a1;
+      do (sl2, a2) <- transl_valof (Csyntax.typeof l) a1;
       ret (finish dst (sl1 ++ sl2) a2)
-  | C.Eaddrof l ty =>
+  | Csyntax.Eaddrof l ty =>
       do (sl, a) <- transl_expr For_val l;
       ret (finish dst sl (Eaddrof a ty))
-  | C.Eunop op r1 ty =>
+  | Csyntax.Eunop op r1 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       ret (finish dst sl1 (Eunop op a1 ty))
-  | C.Ebinop op r1 r2 ty =>
+  | Csyntax.Ebinop op r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       do (sl2, a2) <- transl_expr For_val r2;
       ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty))
-  | C.Ecast r1 ty =>
+  | Csyntax.Ecast r1 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       ret (finish dst sl1 (Ecast a1 ty))
-  | C.Eseqand r1 r2 ty =>
+  | Csyntax.Eseqand r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       match dst with
       | For_val =>
@@ -265,7 +263,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
                makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil,
                dummy_expr)
       end
-  | C.Eseqor r1 r2 ty =>
+  | Csyntax.Eseqor r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       match dst with
       | For_val =>
@@ -283,7 +281,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
                makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil,
                dummy_expr)
       end
-  | C.Econdition r1 r2 r3 ty =>
+  | Csyntax.Econdition r1 r2 r3 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       match dst with
       | For_val =>
@@ -303,11 +301,11 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
           ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
                dummy_expr)
       end
-  | C.Eassign l1 r2 ty =>
+  | Csyntax.Eassign l1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val l1;
       do (sl2, a2) <- transl_expr For_val r2;
-      let ty1 := C.typeof l1 in
-      let ty2 := C.typeof r2 in
+      let ty1 := Csyntax.typeof l1 in
+      let ty2 := Csyntax.typeof r2 in
       match dst with
       | For_val | For_set _ _ =>
           do t <- gensym ty2;
@@ -318,8 +316,8 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
           ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil,
                dummy_expr)
       end
-  | C.Eassignop op l1 r2 tyres ty =>
-      let ty1 := C.typeof l1 in
+  | Csyntax.Eassignop op l1 r2 tyres ty =>
+      let ty1 := Csyntax.typeof l1 in
       do (sl1, a1) <- transl_expr For_val l1;
       do (sl2, a2) <- transl_expr For_val r2;
       do (sl3, a3) <- transl_valof ty1 a1;
@@ -335,8 +333,8 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
           ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil,
                dummy_expr)
       end
-  | C.Epostincr id l1 ty =>
-      let ty1 := C.typeof l1 in
+  | Csyntax.Epostincr id l1 ty =>
+      let ty1 := Csyntax.typeof l1 in
       do (sl1, a1) <- transl_expr For_val l1;
       match dst with
       | For_val | For_set _ _ =>
@@ -350,11 +348,11 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
           ret (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil,
                dummy_expr)
       end
-  | C.Ecomma r1 r2 ty =>
+  | Csyntax.Ecomma r1 r2 ty =>
       do (sl1, a1) <- transl_expr For_effects r1;
       do (sl2, a2) <- transl_expr dst r2;
       ret (sl1 ++ sl2, a2)
-  | C.Ecall r1 rl2 ty =>
+  | Csyntax.Ecall r1 rl2 ty =>
       do (sl1, a1) <- transl_expr For_val r1;
       do (sl2, al2) <- transl_exprlist rl2;
       match dst with
@@ -365,7 +363,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
       | For_effects =>
           ret (sl1 ++ sl2 ++ Scall None a1 al2 :: nil, dummy_expr)
       end
-  | C.Ebuiltin ef tyargs rl ty =>
+  | Csyntax.Ebuiltin ef tyargs rl ty =>
       do (sl, al) <- transl_exprlist rl;
       match dst with
       | For_val | For_set _ _ =>
@@ -375,33 +373,33 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
       | For_effects =>
           ret (sl ++ Sbuiltin None ef tyargs al :: nil, dummy_expr)
       end
-  | C.Eparen r1 ty =>
+  | Csyntax.Eparen r1 ty =>
       error (msg "SimplExpr.transl_expr: paren")
   end
 
 with transl_exprlist (rl: exprlist) : mon (list statement * list expr) :=
   match rl with
-  | C.Enil =>
+  | Csyntax.Enil =>
       ret (nil, nil)
-  | C.Econs r1 rl2 =>
+  | Csyntax.Econs r1 rl2 =>
       do (sl1, a1) <- transl_expr For_val r1;
       do (sl2, al2) <- transl_exprlist rl2;
       ret (sl1 ++ sl2, a1 :: al2)
   end.
 
-Definition transl_expression (r: C.expr) : mon (statement * expr) :=
+Definition transl_expression (r: Csyntax.expr) : mon (statement * expr) :=
   do (sl, a) <- transl_expr For_val r; ret (makeseq sl, a).
 
-Definition transl_expr_stmt (r: C.expr) : mon statement :=
+Definition transl_expr_stmt (r: Csyntax.expr) : mon statement :=
   do (sl, a) <- transl_expr For_effects r; ret (makeseq sl).
 
 (*
-Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement :=
+Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement :=
   do (sl, a) <- transl_expr For_val r;
   ret (makeseq (sl ++ makeif a s1 s2 :: nil)).
 *)
 
-Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement :=
+Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement :=
   do (sl, a) <- transl_expr For_val r;
   ret (makeseq (sl ++ makeif a s1 s2 :: nil)).
 
@@ -410,33 +408,33 @@ Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement :=
 Definition expr_true := Econst_int Int.one type_int32s.
 
 Definition is_Sskip:
-  forall s, {s = C.Sskip} + {s <> C.Sskip}.
+  forall s, {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}.
 Proof.
   destruct s; ((left; reflexivity) || (right; congruence)).
 Defined.
 
-Fixpoint transl_stmt (s: C.statement) : mon statement :=
+Fixpoint transl_stmt (s: Csyntax.statement) : mon statement :=
   match s with
-  | C.Sskip => ret Sskip
-  | C.Sdo e => transl_expr_stmt e
-  | C.Ssequence s1 s2 =>
+  | Csyntax.Sskip => ret Sskip
+  | Csyntax.Sdo e => transl_expr_stmt e
+  | Csyntax.Ssequence s1 s2 =>
       do ts1 <- transl_stmt s1;
       do ts2 <- transl_stmt s2;
       ret (Ssequence ts1 ts2)
-  | C.Sifthenelse e s1 s2 =>
+  | Csyntax.Sifthenelse e s1 s2 =>
       do ts1 <- transl_stmt s1;
       do ts2 <- transl_stmt s2;
       do (s', a) <- transl_expression e;
       ret (Ssequence s' (Sifthenelse a ts1 ts2))
-  | C.Swhile e s1 =>
+  | Csyntax.Swhile e s1 =>
       do s' <- transl_if e Sskip Sbreak;
       do ts1 <- transl_stmt s1;
       ret (Sloop (Ssequence s' ts1) Sskip)
-  | C.Sdowhile e s1 =>
+  | Csyntax.Sdowhile e s1 =>
       do s' <- transl_if e Sskip Sbreak;
       do ts1 <- transl_stmt s1;
       ret (Sloop ts1 s')
-  | C.Sfor s1 e2 s3 s4 =>
+  | Csyntax.Sfor s1 e2 s3 s4 =>
       do ts1 <- transl_stmt s1;
       do s' <- transl_if e2 Sskip Sbreak;
       do ts3 <- transl_stmt s3;
@@ -445,32 +443,32 @@ Fixpoint transl_stmt (s: C.statement) : mon statement :=
         ret (Sloop (Ssequence s' ts4) ts3)
       else
         ret (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3))
-  | C.Sbreak =>
+  | Csyntax.Sbreak =>
       ret Sbreak
-  | C.Scontinue =>
+  | Csyntax.Scontinue =>
       ret Scontinue
-  | C.Sreturn None =>
+  | Csyntax.Sreturn None =>
       ret (Sreturn None)
-  | C.Sreturn (Some e) =>
+  | Csyntax.Sreturn (Some e) =>
       do (s', a) <- transl_expression e;
       ret (Ssequence s' (Sreturn (Some a)))
-  | C.Sswitch e ls =>
+  | Csyntax.Sswitch e ls =>
       do (s', a) <- transl_expression e;
       do tls <- transl_lblstmt ls;
       ret (Ssequence s' (Sswitch a tls))
-  | C.Slabel lbl s1 =>
+  | Csyntax.Slabel lbl s1 =>
       do ts1 <- transl_stmt s1;
       ret (Slabel lbl ts1)
-  | C.Sgoto lbl =>
+  | Csyntax.Sgoto lbl =>
       ret (Sgoto lbl)
   end
 
-with transl_lblstmt (ls: C.labeled_statements) : mon labeled_statements :=
+with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements :=
   match ls with
-  | C.LSdefault s =>
+  | Csyntax.LSdefault s =>
       do ts <- transl_stmt s;
       ret (LSdefault ts)
-  | C.LScase n s ls1 =>
+  | Csyntax.LScase n s ls1 =>
       do ts <- transl_stmt s;
       do tls1 <- transl_lblstmt ls1;
       ret (LScase n ts tls1)
@@ -478,30 +476,30 @@ with transl_lblstmt (ls: C.labeled_statements) : mon labeled_statements :=
 
 (** Translation of a function *)
 
-Definition transl_function (f: C.function) : res function :=
-  match transl_stmt f.(C.fn_body) (initial_generator tt) with
+Definition transl_function (f: Csyntax.function) : res function :=
+  match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with
   | Err msg =>
       Error msg
   | Res tbody g i =>
       OK (mkfunction
-              f.(C.fn_return)
-              f.(C.fn_params)
-              f.(C.fn_vars)
+              f.(Csyntax.fn_return)
+              f.(Csyntax.fn_params)
+              f.(Csyntax.fn_vars)
               g.(gen_trail)
               tbody)
   end.
 
 Local Open Scope error_monad_scope.
 
-Definition transl_fundef (fd: C.fundef) : res fundef :=
+Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
   match fd with
-  | C.Internal f =>
+  | Csyntax.Internal f =>
       do tf <- transl_function f; OK (Internal tf)
-  | C.External ef targs tres =>
+  | Csyntax.External ef targs tres =>
       OK (External ef targs tres)
   end.
 
-Definition transl_program (p: C.program) : res program :=
+Definition transl_program (p: Csyntax.program) : res program :=
   transform_partial_program transl_fundef p.
 
 
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 59fc9bc..150ed76 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -33,7 +33,7 @@ Require Import SimplExprspec.
 
 Section PRESERVATION.
 
-Variable prog: C.program.
+Variable prog: Csyntax.program.
 Variable tprog: Clight.program.
 Hypothesis TRANSL: transl_program prog = OK tprog.
 
@@ -76,20 +76,20 @@ Qed.
 
 Lemma type_of_fundef_preserved:
   forall f tf, transl_fundef f = OK tf ->
-  type_of_fundef tf = C.type_of_fundef f.
+  type_of_fundef tf = Csyntax.type_of_fundef f.
 Proof.
   intros. destruct f; monadInv H.
   exploit transl_function_spec; eauto. intros [A [B [C D]]].
-  simpl. unfold type_of_function, C.type_of_function. congruence.
+  simpl. unfold type_of_function, Csyntax.type_of_function. congruence.
   auto.
 Qed.
 
 Lemma function_return_preserved:
   forall f tf, transl_function f = OK tf ->
-  fn_return tf = C.fn_return f.
+  fn_return tf = Csyntax.fn_return f.
 Proof.
   intros. unfold transl_function in H.
-  destruct (transl_stmt (C.fn_body f) (initial_generator tt)); inv H.
+  destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H.
   auto.
 Qed.
 
@@ -190,11 +190,11 @@ Lemma tr_simple:
   forall le dst sl a tmps,
   tr_expr le dst r sl a tmps ->
   match dst with
-  | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v
+  | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
   | For_effects => sl = nil
   | For_set tyl t =>
       exists b, sl = do_set t tyl b
-             /\ C.typeof r = typeof b
+             /\ Csyntax.typeof r = typeof b
              /\ eval_expr tge e le m b v
   end)
 /\
@@ -202,7 +202,7 @@ Lemma tr_simple:
   eval_simple_lvalue ge e m l b ofs ->
   forall le sl a tmps,
   tr_expr le For_val l sl a tmps ->
-  sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs).
+  sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs).
 Proof.
 Opaque makeif.
   intros e m.
@@ -275,11 +275,11 @@ Lemma tr_simple_rvalue:
   forall le dst sl a tmps,
   tr_expr le dst r sl a tmps ->
   match dst with
-  | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v
+  | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
   | For_effects => sl = nil
   | For_set tyl t =>
       exists b, sl = do_set t tyl b
-             /\ C.typeof r = typeof b
+             /\ Csyntax.typeof r = typeof b
              /\ eval_expr tge e le m b v
   end.
 Proof.
@@ -291,7 +291,7 @@ Lemma tr_simple_lvalue:
   eval_simple_lvalue ge e m l b ofs ->
   forall le sl a tmps,
   tr_expr le For_val l sl a tmps ->
-  sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs.
+  sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs.
 Proof.
   intros e m. exact (proj2 (tr_simple e m)).
 Qed.
@@ -315,8 +315,8 @@ Qed.
 
 Lemma typeof_context:
   forall k1 k2 C, leftcontext k1 k2 C ->
-  forall e1 e2, C.typeof e1 = C.typeof e2 ->
-  C.typeof (C e1) = C.typeof (C e2).
+  forall e1 e2, Csyntax.typeof e1 = Csyntax.typeof e2 ->
+  Csyntax.typeof (C e1) = Csyntax.typeof (C e2).
 Proof.
   induction 1; intros; auto. 
 Qed.
@@ -337,7 +337,7 @@ Lemma tr_expr_leftcontext_rec:
   /\ (forall le' e' sl3,
         tr_expr le' dst' e' sl3 a' tmp' ->
         (forall id, ~In id tmp' -> le'!id = le!id) ->
-        C.typeof e' = C.typeof e ->
+        Csyntax.typeof e' = Csyntax.typeof e ->
         tr_expr le' dst (C e') (sl3 ++ sl2) a tmps)
  ) /\ (
   forall from C, leftcontextlist from C ->
@@ -350,7 +350,7 @@ Lemma tr_expr_leftcontext_rec:
   /\ (forall le' e' sl3,
         tr_expr le' dst' e' sl3 a' tmp' ->
         (forall id, ~In id tmp' -> le'!id = le!id) ->
-        C.typeof e' = C.typeof e ->
+        Csyntax.typeof e' = Csyntax.typeof e ->
         tr_exprlist le' (C e') (sl3 ++ sl2) a tmps)
 ).
 Proof.
@@ -695,7 +695,7 @@ Theorem tr_expr_leftcontext:
   /\ (forall le' r' sl3,
         tr_expr le' dst' r' sl3 a' tmp' ->
         (forall id, ~In id tmp' -> le'!id = le!id) ->
-        C.typeof r' = C.typeof r ->
+        Csyntax.typeof r' = Csyntax.typeof r ->
         tr_expr le' dst (C r') (sl3 ++ sl2) a tmps).
 Proof.
   intros. eapply (proj1 tr_expr_leftcontext_rec); eauto.
@@ -714,7 +714,7 @@ Theorem tr_top_leftcontext:
   /\ (forall le' m' r' sl3,
         tr_expr le' dst' r' sl3 a' tmp' ->
         (forall id, ~In id tmp' -> le'!id = le!id) ->
-        C.typeof r' = C.typeof r ->
+        Csyntax.typeof r' = Csyntax.typeof r ->
         tr_top tge e le' m' dst (C r') (sl3 ++ sl2) a tmps).
 Proof.
   induction 1; intros.
@@ -895,7 +895,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop :=
   | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps,
       transl_function f = Errors.OK tf ->
       leftcontext RV RV C ->
-      (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (C.Eval v ty)) sl a tmps) ->
+      (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) ->
       match_cont_exp dest a k tk ->
       match_cont (Csem.Kcall f e C ty k)
                  (Kcall optid tf e le (Kseqlist sl tk))
@@ -1220,10 +1220,10 @@ Proof.
 (* for not skip *)
   rename s' into sr.
   rewrite (tr_find_label_if _ _ H3); auto.
-  exploit (IHs1 (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)); eauto. 
+  exploit (IHs1 (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)); eauto. 
     econstructor; eauto. econstructor; eauto. 
   destruct (Csem.find_label lbl s1
-               (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)) as [[s' k'] | ].
+               (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)) as [[s' k'] | ].
   intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
   intro EQ; rewrite EQ.
   exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto.
@@ -1265,49 +1265,49 @@ End FIND_LABEL.
     Sdo a, k  --->  a, Kdo k ---> rval v, Kdo k ---> Sskip, k
 >>
   but the translation, which is [Sskip], makes no transitions.
-- The reduction [C.Ecomma (C.Eval v) r2 --> r2].
-- The reduction [C.Eparen (C.Eval v) --> C.Eval v] in a [For_effects] context.
+- The reduction [Ecomma (Eval v) r2 --> r2].
+- The reduction [Eparen (Eval v) --> Eval v] in a [For_effects] context.
 
 The following measure decreases for these stuttering steps. *)
 
-Fixpoint esize (a: C.expr) : nat :=
+Fixpoint esize (a: Csyntax.expr) : nat :=
   match a with
-  | C.Eloc _ _ _ => 1%nat
-  | C.Evar _ _ => 1%nat
-  | C.Ederef r1 _ => S(esize r1)
-  | C.Efield l1 _ _ => S(esize l1)
-  | C.Eval _ _ => O
-  | C.Evalof l1 _ => S(esize l1)
-  | C.Eaddrof l1 _ => S(esize l1)
-  | C.Eunop _ r1 _ => S(esize r1)
-  | C.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat
-  | C.Ecast r1 _ => S(esize r1)
-  | C.Eseqand r1 _ _ => S(esize r1)
-  | C.Eseqor r1 _ _ => S(esize r1)
-  | C.Econdition r1 _ _ _ => S(esize r1)
-  | C.Esizeof _ _ => 1%nat
-  | C.Ealignof _ _ => 1%nat
-  | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat
-  | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat
-  | C.Epostincr _ l1 _ => S(esize l1)
-  | C.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat
-  | C.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat
-  | C.Ebuiltin ef _ rl _ => S(esizelist rl)%nat
-  | C.Eparen r1 _ => S(esize r1)
+  | Csyntax.Eloc _ _ _ => 1%nat
+  | Csyntax.Evar _ _ => 1%nat
+  | Csyntax.Ederef r1 _ => S(esize r1)
+  | Csyntax.Efield l1 _ _ => S(esize l1)
+  | Csyntax.Eval _ _ => O
+  | Csyntax.Evalof l1 _ => S(esize l1)
+  | Csyntax.Eaddrof l1 _ => S(esize l1)
+  | Csyntax.Eunop _ r1 _ => S(esize r1)
+  | Csyntax.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat
+  | Csyntax.Ecast r1 _ => S(esize r1)
+  | Csyntax.Eseqand r1 _ _ => S(esize r1)
+  | Csyntax.Eseqor r1 _ _ => S(esize r1)
+  | Csyntax.Econdition r1 _ _ _ => S(esize r1)
+  | Csyntax.Esizeof _ _ => 1%nat
+  | Csyntax.Ealignof _ _ => 1%nat
+  | Csyntax.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat
+  | Csyntax.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat
+  | Csyntax.Epostincr _ l1 _ => S(esize l1)
+  | Csyntax.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat
+  | Csyntax.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat
+  | Csyntax.Ebuiltin ef _ rl _ => S(esizelist rl)%nat
+  | Csyntax.Eparen r1 _ => S(esize r1)
   end
 
-with esizelist (el: C.exprlist) : nat :=
+with esizelist (el: Csyntax.exprlist) : nat :=
   match el with
-  | C.Enil => O
-  | C.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat
+  | Csyntax.Enil => O
+  | Csyntax.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat
   end.
 
 Definition measure (st: Csem.state) : nat :=
   match st with
   | Csem.ExprState _ r _ _ _ => (esize r + 1)%nat
-  | Csem.State _ C.Sskip _ _ _ => 0%nat
-  | Csem.State _ (C.Sdo r) _ _ _ => (esize r + 2)%nat
-  | Csem.State _ (C.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat
+  | Csem.State _ Csyntax.Sskip _ _ _ => 0%nat
+  | Csem.State _ (Csyntax.Sdo r) _ _ _ => (esize r + 2)%nat
+  | Csem.State _ (Csyntax.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat
   | _ => 0%nat
   end.
 
@@ -1338,7 +1338,7 @@ Lemma tr_val_gen:
   (forall tge e le' m,
       (forall id, In id tmp -> le'!id = le!id) ->
       eval_expr tge e le' m a v) ->
-  tr_expr le dst (C.Eval v ty) (final dst a) a tmp.
+  tr_expr le dst (Csyntax.Eval v ty) (final dst a) a tmp.
 Proof.
   intros. destruct dst; simpl; econstructor; auto.
 Qed.
@@ -1378,7 +1378,7 @@ Proof.
   econstructor; split.
   left. eapply plus_two. constructor. eapply step_make_set; eauto. traceEq. 
   econstructor; eauto.
-  change (final dst' (Etempvar t0 (C.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (C.typeof l)) ++ sl2)).
+  change (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2)).
   apply S. apply tr_val_gen. auto. 
   intros. constructor. rewrite H5; auto. apply PTree.gss.
   intros. apply PTree.gso. red; intros; subst; elim H5; auto. 
@@ -1784,7 +1784,7 @@ Proof.
   left. eapply plus_left. constructor. apply star_one.
   econstructor. econstructor; eauto. rewrite <- TY1; eauto. traceEq.
   econstructor; eauto. 
-  change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S.
+  change sl2 with (final For_val (Etempvar t (Csyntax.typeof r)) ++ sl2). apply S.
   constructor. auto. intros. constructor. rewrite H2; auto. apply PTree.gss.
   intros. apply PTree.gso. intuition congruence.
   auto. 
@@ -1877,7 +1877,7 @@ Qed.
 
 Lemma tr_top_val_for_val_inv:
   forall e le m v ty sl a tmps,
-  tr_top tge e le m For_val (C.Eval v ty) sl a tmps ->
+  tr_top tge e le m For_val (Csyntax.Eval v ty) sl a tmps ->
   sl = nil /\ typeof a = ty /\ eval_expr tge e le m a v.
 Proof.
   intros. inv H. auto. inv H0. auto. 
@@ -2087,7 +2087,7 @@ Proof.
   inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
   econstructor; split.
   left. eapply plus_two. constructor. econstructor. eauto.
-  replace (fn_return tf) with (C.fn_return f). eauto.
+  replace (fn_return tf) with (Csyntax.fn_return f). eauto.
   exploit transl_function_spec; eauto. intuition congruence. 
   eauto. traceEq.
   constructor. apply match_cont_call; auto.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 571a937..5cb0f18 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -35,9 +35,9 @@ Local Open Scope gensym_monad_scope.
 
 (** This specification covers:
 - all cases of [transl_lvalue] and [transl_rvalue];
-- two additional cases for [C.Eparen], so that reductions of [C.Econdition]
+- two additional cases for [Csyntax.Eparen], so that reductions of [Csyntax.Econdition]
   expressions are properly tracked;
-- three additional cases allowing [C.Eval v] C expressions to match
+- three additional cases allowing [Csyntax.Eval v] C expressions to match
   any Clight expression [a] that evaluates to [v] in any environment
   matching the given temporary environment [le].
 *)
@@ -57,69 +57,69 @@ Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Pro
       type_is_volatile ty = true -> In t tmp ->
       tr_rvalof ty a (make_set t a :: nil) (Etempvar t ty) tmp.
 
-Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop :=
+Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop :=
   | tr_var: forall le dst id ty tmp,
-      tr_expr le dst (C.Evar id ty)
+      tr_expr le dst (Csyntax.Evar id ty)
               (final dst (Evar id ty)) (Evar id ty) tmp
   | tr_deref: forall le dst e1 ty sl1 a1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp ->
-      tr_expr le dst (C.Ederef e1 ty)
+      tr_expr le dst (Csyntax.Ederef e1 ty)
               (sl1 ++ final dst (Ederef a1 ty)) (Ederef a1 ty) tmp
   | tr_field: forall le dst e1 f ty sl1 a1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp ->
-      tr_expr le dst (C.Efield e1 f ty)
+      tr_expr le dst (Csyntax.Efield e1 f ty)
               (sl1 ++ final dst (Efield a1 f ty)) (Efield a1 f ty) tmp
   | tr_val_effect: forall le v ty any tmp,
-      tr_expr le For_effects (C.Eval v ty) nil any tmp
+      tr_expr le For_effects (Csyntax.Eval v ty) nil any tmp
   | tr_val_value: forall le v ty a tmp,
       typeof a = ty ->
       (forall tge e le' m,
          (forall id, In id tmp -> le'!id = le!id) ->
          eval_expr tge e le' m a v) ->
-      tr_expr le For_val (C.Eval v ty) 
+      tr_expr le For_val (Csyntax.Eval v ty) 
                            nil a tmp
   | tr_val_set: forall le tyl t v ty a any tmp,
       typeof a = ty ->
       (forall tge e le' m,
          (forall id, In id tmp -> le'!id = le!id) ->
          eval_expr tge e le' m a v) ->
-      tr_expr le (For_set tyl t) (C.Eval v ty) 
+      tr_expr le (For_set tyl t) (Csyntax.Eval v ty) 
                    (do_set t tyl a) any tmp
   | tr_sizeof: forall le dst ty' ty tmp,
-      tr_expr le dst (C.Esizeof ty' ty)
+      tr_expr le dst (Csyntax.Esizeof ty' ty)
                    (final dst (Esizeof ty' ty))
                    (Esizeof ty' ty) tmp
   | tr_alignof: forall le dst ty' ty tmp,
-      tr_expr le dst (C.Ealignof ty' ty)
+      tr_expr le dst (Csyntax.Ealignof ty' ty)
                    (final dst (Ealignof ty' ty))
                    (Ealignof ty' ty) tmp
   | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
-      tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 ->
+      tr_rvalof (Csyntax.typeof e1) a1 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le dst (C.Evalof e1 ty)
+      tr_expr le dst (Csyntax.Evalof e1 ty)
                     (sl1 ++ sl2 ++ final dst a2)
                     a2 tmp
   | tr_addrof: forall le dst e1 ty tmp sl1 a1,
       tr_expr le For_val e1 sl1 a1 tmp ->
-      tr_expr le dst (C.Eaddrof e1 ty) 
+      tr_expr le dst (Csyntax.Eaddrof e1 ty) 
                    (sl1 ++ final dst (Eaddrof a1 ty))
                    (Eaddrof a1 ty) tmp
   | tr_unop: forall le dst op e1 ty tmp sl1 a1,
       tr_expr le For_val e1 sl1 a1 tmp ->
-      tr_expr le dst (C.Eunop op e1 ty)
+      tr_expr le dst (Csyntax.Eunop op e1 ty)
                    (sl1 ++ final dst (Eunop op a1 ty))
                    (Eunop op a1 ty) tmp
   | tr_binop: forall le dst op e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le dst (C.Ebinop op e1 e2 ty)
+      tr_expr le dst (Csyntax.Ebinop op e1 e2 ty)
                    (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty))
                    (Ebinop op a1 a2 ty) tmp
   | tr_cast: forall le dst e1 ty sl1 a1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp ->
-      tr_expr le dst (C.Ecast e1 ty)
+      tr_expr le dst (Csyntax.Ecast e1 ty)
                    (sl1 ++ final dst (Ecast a1 ty))
                    (Ecast a1 ty) tmp
   | tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
@@ -127,7 +127,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le For_val (C.Eseqand e1 e2 ty)
+      tr_expr le For_val (Csyntax.Eseqand e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq sl2)
                                       (Sset t (Econst_int Int.zero ty)) :: nil)
                     (Etempvar t ty) tmp
@@ -136,7 +136,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le For_effects e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le For_effects (C.Eseqand e1 e2 ty)
+      tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil)
                     any tmp
   | tr_seqand_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
@@ -144,7 +144,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (C.Eseqand e1 e2 ty)
+      tr_expr le (For_set tyl t) (Csyntax.Eseqand e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq sl2)
                                       (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil)
                     any tmp
@@ -153,7 +153,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le For_val (C.Eseqor e1 e2 ty)
+      tr_expr le For_val (Csyntax.Eseqor e1 e2 ty)
                     (sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty))
                                       (makeseq sl2) :: nil)
                     (Etempvar t ty) tmp
@@ -162,7 +162,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le For_effects e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le For_effects (C.Eseqor e1 e2 ty)
+      tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty)
                     (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil)
                     any tmp
   | tr_seqor_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
@@ -170,7 +170,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (C.Eseqor e1 e2 ty)
+      tr_expr le (For_set tyl t) (Csyntax.Eseqor e1 e2 ty)
                     (sl1 ++ makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty)))
                                       (makeseq sl2) :: nil)
                     any tmp
@@ -181,7 +181,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       list_disjoint tmp1 tmp2 ->
       list_disjoint tmp1 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp ->  incl tmp3 tmp -> In t tmp ->
-      tr_expr le For_val (C.Econdition e1 e2 e3 ty)
+      tr_expr le For_val (Csyntax.Econdition e1 e2 e3 ty)
                       (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                       (Etempvar t ty) tmp
   | tr_condition_effects: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
@@ -191,7 +191,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       list_disjoint tmp1 tmp2 ->
       list_disjoint tmp1 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
-      tr_expr le For_effects (C.Econdition e1 e2 e3 ty)
+      tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty)
                        (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                        any tmp
   | tr_condition_set: forall le tyl t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
@@ -201,7 +201,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       list_disjoint tmp1 tmp2 ->
       list_disjoint tmp1 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
-      tr_expr le (For_set tyl t) (C.Econdition e1 e2 e3 ty)
+      tr_expr le (For_set tyl t) (Csyntax.Econdition e1 e2 e3 ty)
                        (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                        any tmp
   | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
@@ -209,7 +209,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->  
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le For_effects (C.Eassign e1 e2 ty)
+      tr_expr le For_effects (Csyntax.Eassign e1 e2 ty)
                       (sl1 ++ sl2 ++ make_assign a1 a2 :: nil)
                       any tmp
   | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2,
@@ -218,9 +218,9 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       incl tmp1 tmp -> incl tmp2 tmp ->
       list_disjoint tmp1 tmp2 ->  
       In t tmp -> ~In t tmp1 -> ~In t tmp2 ->
-      ty1 = C.typeof e1 ->
-      ty2 = C.typeof e2 ->
-      tr_expr le dst (C.Eassign e1 e2 ty)
+      ty1 = Csyntax.typeof e1 ->
+      ty2 = Csyntax.typeof e2 ->
+      tr_expr le dst (Csyntax.Eassign e1 e2 ty)
                    (sl1 ++ sl2 ++ 
                     Sset t a2 ::
                     make_assign a1 (Etempvar t ty2) ::
@@ -229,11 +229,11 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
   | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
-      ty1 = C.typeof e1 ->
+      ty1 = Csyntax.typeof e1 ->
       tr_rvalof ty1 a1 sl3 a3 tmp3 ->
       list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
-      tr_expr le For_effects (C.Eassignop op e1 e2 tyres ty)
+      tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty)
                       (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil)
                       any tmp
   | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1,
@@ -243,8 +243,8 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
       In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 ->
-      ty1 = C.typeof e1 ->
-      tr_expr le dst (C.Eassignop op e1 e2 tyres ty)
+      ty1 = Csyntax.typeof e1 ->
+      tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty)
                    (sl1 ++ sl2 ++ sl3 ++
                     Sset t (Ebinop op a3 a2 tyres) ::
                     make_assign a1 (Etempvar t tyres) ::
@@ -253,17 +253,17 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
   | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_rvalof ty1 a1 sl2 a2 tmp2 ->
-      ty1 = C.typeof e1 ->
+      ty1 = Csyntax.typeof e1 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
       list_disjoint tmp1 tmp2 ->  
-      tr_expr le For_effects (C.Epostincr id e1 ty)
+      tr_expr le For_effects (Csyntax.Epostincr id e1 ty)
                       (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil)
                       any tmp
   | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       incl tmp1 tmp -> In t tmp -> ~In t tmp1 ->
-      ty1 = C.typeof e1 ->
-      tr_expr le dst (C.Epostincr id e1 ty)
+      ty1 = Csyntax.typeof e1 ->
+      tr_expr le dst (Csyntax.Epostincr id e1 ty)
                    (sl1 ++ make_set t a1 ::
                     make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) ::
                     final dst (Etempvar t ty1))
@@ -273,13 +273,13 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le dst e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->  
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le dst (C.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp
+      tr_expr le dst (Csyntax.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp
   | tr_call_effects: forall le e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_exprlist le el2 sl2 al2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le For_effects (C.Ecall e1 el2 ty)
+      tr_expr le For_effects (Csyntax.Ecall e1 el2 ty)
                    (sl1 ++ sl2 ++ Scall None a1 al2 :: nil)
                    any tmp
   | tr_call_val: forall le dst e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 t tmp,
@@ -288,45 +288,45 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_exprlist le el2 sl2 al2 tmp2 ->
       list_disjoint tmp1 tmp2 -> In t tmp ->
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_expr le dst (C.Ecall e1 el2 ty)
+      tr_expr le dst (Csyntax.Ecall e1 el2 ty)
                    (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: final dst (Etempvar t ty))
                    (Etempvar t ty) tmp
   | tr_builtin_effects: forall le ef tyargs el ty sl al tmp1 any tmp,
       tr_exprlist le el sl al tmp1 ->
       incl tmp1 tmp ->
-      tr_expr le For_effects (C.Ebuiltin ef tyargs el ty)
+      tr_expr le For_effects (Csyntax.Ebuiltin ef tyargs el ty)
                    (sl ++ Sbuiltin None ef tyargs al :: nil)
                    any tmp
   | tr_builtin_val: forall le dst ef tyargs el ty sl al tmp1 t tmp,
       dst <> For_effects ->
       tr_exprlist le el sl al tmp1 ->
       In t tmp -> incl tmp1 tmp ->
-      tr_expr le dst (C.Ebuiltin ef tyargs el ty)
+      tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty)
                    (sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty))
                    (Etempvar t ty) tmp
   | tr_paren_val: forall le e1 ty sl1 a1 t tmp,
       tr_expr le (For_set (ty :: nil) t) e1 sl1 a1 tmp ->
       In t tmp -> 
-      tr_expr le For_val (C.Eparen e1 ty)
+      tr_expr le For_val (Csyntax.Eparen e1 ty)
                        sl1
                        (Etempvar t ty) tmp
   | tr_paren_effects: forall le e1 ty sl1 a1 tmp any,
       tr_expr le For_effects e1 sl1 a1 tmp ->
-      tr_expr le For_effects (C.Eparen e1 ty) sl1 any tmp
+      tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp
   | tr_paren_set: forall le tyl t e1 ty sl1 a1 tmp any,
       tr_expr le (For_set (ty::tyl) t) e1 sl1 a1 tmp ->
       In t tmp ->
-      tr_expr le (For_set tyl t) (C.Eparen e1 ty) sl1 any tmp
+      tr_expr le (For_set tyl t) (Csyntax.Eparen e1 ty) sl1 any tmp
 
-with tr_exprlist: temp_env -> C.exprlist -> list statement -> list expr -> list ident -> Prop :=
+with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop :=
   | tr_nil: forall le tmp,
-      tr_exprlist le C.Enil nil nil tmp
+      tr_exprlist le Csyntax.Enil nil nil tmp
   | tr_cons: forall le e1 el2 sl1 a1 tmp1 sl2 al2 tmp2 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_exprlist le el2 sl2 al2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
-      tr_exprlist le (C.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp.
+      tr_exprlist le (Csyntax.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp.
 
 Scheme tr_expr_ind2 := Minimality for tr_expr Sort Prop
   with tr_exprlist_ind2 := Minimality for tr_exprlist Sort Prop.
@@ -372,11 +372,11 @@ Qed.
 
 (** The "top-level" translation is equivalent to [tr_expr] above
   for source terms.  It brings additional flexibility in the matching
-  between C values and Cminor expressions: in the case of
+  between Csyntax values and Cminor expressions: in the case of
   [tr_expr], the Cminor expression must not depend on memory,
   while in the case of [tr_top] it can depend on the current memory
   state.  This special case is extended to values occurring under
-  one or several [C.Eparen]. *)
+  one or several [Csyntax.Eparen]. *)
 
 Section TR_TOP.
 
@@ -385,14 +385,14 @@ Variable e: env.
 Variable le: temp_env.
 Variable m: mem.
 
-Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident -> Prop :=
+Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop :=
   | tr_top_val_val: forall v ty a tmp,
       typeof a = ty -> eval_expr ge e le m a v ->
-      tr_top For_val (C.Eval v ty) nil a tmp
+      tr_top For_val (Csyntax.Eval v ty) nil a tmp
 (*
   | tr_top_val_set: forall t tyl v ty a any tmp,
       typeof a = ty -> eval_expr ge e le m a v ->
-      tr_top (For_set tyl t) (C.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp
+      tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp
 *)
   | tr_top_base: forall dst r sl a tmp,
       tr_expr le dst r sl a tmp ->
@@ -400,92 +400,92 @@ Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident
 (*
   | tr_top_paren_test: forall tyl t r ty sl a tmp,
       tr_top (For_set (ty :: tyl) t) r sl a tmp ->
-      tr_top (For_set tyl t) (C.Eparen r ty) sl a tmp.
+      tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp.
 *)
 
 End TR_TOP.
 
 (** ** Translation of statements *)
 
-Inductive tr_expression: C.expr -> statement -> expr -> Prop :=
+Inductive tr_expression: Csyntax.expr -> statement -> expr -> Prop :=
   | tr_expression_intro: forall r sl a tmps,
       (forall ge e le m, tr_top ge e le m For_val r sl a tmps) ->
       tr_expression r (makeseq sl) a.
 
-Inductive tr_expr_stmt: C.expr -> statement -> Prop :=
+Inductive tr_expr_stmt: Csyntax.expr -> statement -> Prop :=
   | tr_expr_stmt_intro: forall r sl a tmps,
       (forall ge e le m, tr_top ge e le m For_effects r sl a tmps) ->
       tr_expr_stmt r (makeseq sl).
 
-Inductive tr_if: C.expr -> statement -> statement -> statement -> Prop :=
+Inductive tr_if: Csyntax.expr -> statement -> statement -> statement -> Prop :=
   | tr_if_intro: forall r s1 s2 sl a tmps,
       (forall ge e le m, tr_top ge e le m For_val r sl a tmps) ->
       tr_if r s1 s2 (makeseq (sl ++ makeif a s1 s2 :: nil)).
 
-Inductive tr_stmt: C.statement -> statement -> Prop :=
+Inductive tr_stmt: Csyntax.statement -> statement -> Prop :=
   | tr_skip:
-      tr_stmt C.Sskip Sskip
+      tr_stmt Csyntax.Sskip Sskip
   | tr_do: forall r s,
       tr_expr_stmt r s ->
-      tr_stmt (C.Sdo r) s
+      tr_stmt (Csyntax.Sdo r) s
   | tr_seq: forall s1 s2 ts1 ts2,
       tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
-      tr_stmt (C.Ssequence s1 s2) (Ssequence ts1 ts2)
+      tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2)
   | tr_ifthenelse: forall r s1 s2 s' a ts1 ts2,
       tr_expression r s' a ->
       tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
-      tr_stmt (C.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2))
+      tr_stmt (Csyntax.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2))
   | tr_while: forall r s1 s' ts1,
       tr_if r Sskip Sbreak s' ->
       tr_stmt s1 ts1 ->
-      tr_stmt (C.Swhile r s1)
+      tr_stmt (Csyntax.Swhile r s1)
               (Sloop (Ssequence s' ts1) Sskip)
   | tr_dowhile: forall r s1 s' ts1,
       tr_if r Sskip Sbreak s' ->
       tr_stmt s1 ts1 ->
-      tr_stmt (C.Sdowhile r s1)
+      tr_stmt (Csyntax.Sdowhile r s1)
               (Sloop ts1 s')
   | tr_for_1: forall r s3 s4 s' ts3 ts4,
       tr_if r Sskip Sbreak s' ->
       tr_stmt s3 ts3 ->
       tr_stmt s4 ts4 ->
-      tr_stmt (C.Sfor C.Sskip r s3 s4)
+      tr_stmt (Csyntax.Sfor Csyntax.Sskip r s3 s4)
               (Sloop (Ssequence s' ts4) ts3)
   | tr_for_2: forall s1 r s3 s4 s' ts1 ts3 ts4,
       tr_if r Sskip Sbreak s' ->
-      s1 <> C.Sskip ->
+      s1 <> Csyntax.Sskip ->
       tr_stmt s1 ts1 ->
       tr_stmt s3 ts3 ->
       tr_stmt s4 ts4 ->
-      tr_stmt (C.Sfor s1 r s3 s4)
+      tr_stmt (Csyntax.Sfor s1 r s3 s4)
               (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3))
   | tr_break:
-      tr_stmt C.Sbreak Sbreak
+      tr_stmt Csyntax.Sbreak Sbreak
   | tr_continue:
-      tr_stmt C.Scontinue Scontinue
+      tr_stmt Csyntax.Scontinue Scontinue
   | tr_return_none:
-      tr_stmt (C.Sreturn None) (Sreturn None)
+      tr_stmt (Csyntax.Sreturn None) (Sreturn None)
   | tr_return_some: forall r s' a,
       tr_expression r s' a ->
-      tr_stmt (C.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a)))
+      tr_stmt (Csyntax.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a)))
   | tr_switch: forall r ls s' a tls,
       tr_expression r s' a ->
       tr_lblstmts ls tls ->
-      tr_stmt (C.Sswitch r ls) (Ssequence s' (Sswitch a tls))
+      tr_stmt (Csyntax.Sswitch r ls) (Ssequence s' (Sswitch a tls))
   | tr_label: forall lbl s ts,
       tr_stmt s ts ->
-      tr_stmt (C.Slabel lbl s) (Slabel lbl ts)
+      tr_stmt (Csyntax.Slabel lbl s) (Slabel lbl ts)
   | tr_goto: forall lbl,
-      tr_stmt (C.Sgoto lbl) (Sgoto lbl)
+      tr_stmt (Csyntax.Sgoto lbl) (Sgoto lbl)
 
-with tr_lblstmts: C.labeled_statements -> labeled_statements -> Prop :=
+with tr_lblstmts: Csyntax.labeled_statements -> labeled_statements -> Prop :=
   | tr_default: forall s ts,
       tr_stmt s ts ->
-      tr_lblstmts (C.LSdefault s) (LSdefault ts)
+      tr_lblstmts (Csyntax.LSdefault s) (LSdefault ts)
   | tr_case: forall n s ls ts tls,
       tr_stmt s ts ->
       tr_lblstmts ls tls ->
-      tr_lblstmts (C.LScase n s ls) (LScase n ts tls).
+      tr_lblstmts (Csyntax.LScase n s ls) (LScase n ts tls).
 
 (** * Correctness proof with respect to the specification. *)
 
@@ -504,7 +504,7 @@ Proof.
 Qed.
 
 Remark bind2_inversion:
-  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (y: C) (z1 z3: generator) I,
+  forall (A B Csyntax: Type) (f: mon (A*B)) (g: A -> B -> mon Csyntax) (y: Csyntax) (z1 z3: generator) I,
   bind2 f g z1 = Res y z3 I ->
   exists x1, exists x2, exists z2, exists I1, exists I2,
   f z1 = Res (x1,x2) z2 I1 /\ g x1 x2 z2 = Res y z3 I2.
@@ -632,7 +632,7 @@ Lemma contained_disjoint:
   contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2.
 Proof.
   intros; red; intros. red; intro; subst y. 
-  exploit H; eauto. intros [A B]. exploit H0; eauto. intros [C D].
+  exploit H; eauto. intros [A B]. exploit H0; eauto. intros [Csyntax D].
   elim (Plt_strict x). apply Plt_Ple_trans with (gen_next g2); auto.
 Qed.
 
@@ -640,7 +640,7 @@ Lemma contained_notin:
   forall g1 l g2 id g3,
   contained l g1 g2 -> within id g2 g3 -> ~In id l.
 Proof.
-  intros; red; intros. exploit H; eauto. intros [C D]. destruct H0 as [A B].
+  intros; red; intros. exploit H; eauto. intros [Csyntax D]. destruct H0 as [A B].
   elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto.
 Qed.
 
@@ -737,13 +737,13 @@ Lemma transl_valof_meets_spec:
   exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'.
 Proof.
   unfold transl_valof; intros.
-  destruct (type_is_volatile ty) as []_eqn; monadInv H.
+  destruct (type_is_volatile ty) eqn:?; monadInv H.
   exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib.
   exists (@nil ident); split; eauto with gensym. constructor; auto.
 Qed.
 
-Scheme expr_ind2 := Induction for C.expr Sort Prop
-  with exprlist_ind2 := Induction for C.exprlist Sort Prop.
+Scheme expr_ind2 := Induction for Csyntax.expr Sort Prop
+  with exprlist_ind2 := Induction for Csyntax.exprlist Sort Prop.
 Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2.
 
 Lemma transl_meets_spec:
@@ -775,7 +775,7 @@ Opaque makeif.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. 
 (* valof *)
   monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
-  exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. UseFinish.
+  exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
@@ -790,7 +790,7 @@ Opaque makeif.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. 
 (* binop *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto. intros [tmp2 [C D]]. UseFinish.
+  exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split. 
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
@@ -801,7 +801,7 @@ Opaque makeif.
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_val; eauto with gensym.
@@ -809,13 +809,13 @@ Opaque makeif.
   apply contained_cons. eauto with gensym. 
   apply contained_app; eauto with gensym.
   (* for effects *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for set *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqand_set; eauto with gensym.
@@ -825,7 +825,7 @@ Opaque makeif.
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_val; eauto with gensym.
@@ -833,13 +833,13 @@ Opaque makeif.
   apply contained_cons. eauto with gensym. 
   apply contained_app; eauto with gensym.
   (* for effects *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_effects; eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for set *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2); split.
   intros; eapply tr_seqor_set; eauto with gensym.
@@ -849,7 +849,7 @@ Opaque makeif.
   monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exploit H1; eauto with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split. 
@@ -860,14 +860,14 @@ Opaque makeif.
   apply contained_app. eauto with gensym.
   apply contained_app; eauto with gensym.
   (* for effects *)
-  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit H1; eauto. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   intros; eapply tr_condition_effects; eauto with gensym. 
   apply contained_app; eauto with gensym.
   (* for test *)
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exploit H1; eauto with gensym. intros [tmp3 [E F]].
   simpl add_dest in *.
   exists (tmp1 ++ tmp2 ++ tmp3); split.
@@ -883,7 +883,7 @@ Opaque makeif.
   exists (@nil ident); split; auto with gensym. constructor.
 (* assign *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split. 
@@ -902,7 +902,7 @@ Opaque makeif.
   apply contained_app; eauto with gensym.
 (* assignop *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
   destruct dst; monadInv EQ3; simpl add_dest in *.
   (* for value *)
@@ -928,7 +928,7 @@ Opaque makeif.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym. 
   (* for effects *)
-  exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]].
+  exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split. 
   econstructor; eauto with gensym.
   eauto with gensym. 
@@ -939,7 +939,7 @@ Opaque makeif.
   apply contained_cons; eauto with gensym. 
 (* comma *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto with gensym. intros [tmp2 [C D]].
+  exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split. 
   econstructor; eauto with gensym.
   destruct dst; simpl; eauto with gensym. 
@@ -949,7 +949,7 @@ Opaque makeif.
   apply contained_app; eauto with gensym.
 (* call *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
   exists (x1 :: tmp1 ++ tmp2); split. 
@@ -988,7 +988,7 @@ Opaque makeif.
   monadInv H; exists (@nil ident); split; auto with gensym. constructor.
 (* cons *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
-  exploit H0; eauto. intros [tmp2 [C D]].
+  exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split. 
   econstructor; eauto with gensym.
   eauto with gensym.
@@ -1054,13 +1054,13 @@ Qed.
 Theorem transl_function_spec:
   forall f tf,
   transl_function f = OK tf ->
-  tr_stmt f.(C.fn_body) tf.(fn_body)
-  /\ fn_return tf = C.fn_return f
-  /\ fn_params tf = C.fn_params f
-  /\ fn_vars tf = C.fn_vars f.
+  tr_stmt f.(Csyntax.fn_body) tf.(fn_body)
+  /\ fn_return tf = Csyntax.fn_return f
+  /\ fn_params tf = Csyntax.fn_params f
+  /\ fn_vars tf = Csyntax.fn_vars f.
 Proof.
   intros until tf. unfold transl_function.
-  case_eq (transl_stmt (C.fn_body f) (initial_generator tt)); intros; inv H0.
+  case_eq (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); intros; inv H0.
   simpl. intuition. eapply transl_stmt_meets_spec; eauto.
 Qed.
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index f58a213..8df7b6e 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -83,7 +83,7 @@ Lemma type_of_global_preserved:
 Proof.
   unfold type_of_global; intros.
   rewrite varinfo_preserved. destruct (Genv.find_var_info ge id). auto. 
-  destruct (Genv.find_funct_ptr ge id) as [fd|]_eqn; inv H.
+  destruct (Genv.find_funct_ptr ge id) as [fd|] eqn:?; inv H.
   exploit function_ptr_translated; eauto. intros [tf [A B]]. rewrite A. 
   decEq. apply type_of_fundef_preserved; auto.
 Qed.
@@ -183,12 +183,12 @@ Lemma match_envs_extcall:
 Proof.
   intros. eapply match_envs_invariant; eauto. 
   intros. destruct H0.  eapply H8. intros; red. auto. auto. 
-  red in H2. intros. destruct (f b) as [[b' delta]|]_eqn. 
+  red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?. 
   eapply H1; eauto.
-  destruct (f' b) as [[b' delta]|]_eqn; auto. 
+  destruct (f' b) as [[b' delta]|] eqn:?; auto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
   omegaContradiction.
-  intros. destruct (f b) as [[b'' delta']|]_eqn. eauto. 
+  intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
   omegaContradiction.
 Qed.
@@ -405,7 +405,7 @@ Lemma match_envs_set_temp:
   match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi.
 Proof.
   intros. unfold check_temp in H1. 
-  destruct (VSet.mem id cenv) as []_eqn; monadInv H1.
+  destruct (VSet.mem id cenv) eqn:?; monadInv H1.
   destruct H. constructor; eauto; intros.
 (* vars *)
   generalize (me_vars0 id0); intros MV; inv MV.
@@ -477,8 +477,8 @@ Remark add_local_variable_charact:
   VSet.In id1 cenv \/ exists chunk, access_mode ty = By_value chunk /\ id = id1 /\ VSet.mem id atk = false.
 Proof.
   intros. unfold add_local_variable. split; intros. 
-  destruct (access_mode ty) as []_eqn; auto.
-  destruct (VSet.mem id atk) as []_eqn; auto.
+  destruct (access_mode ty) eqn:?; auto.
+  destruct (VSet.mem id atk) eqn:?; auto.
   rewrite VSF.add_iff in H. destruct H; auto. right; exists m; auto.
   destruct H as [A | [chunk [A [B C]]]].
   destruct (access_mode ty); auto. destruct (VSet.mem id atk); auto. rewrite VSF.add_iff; auto.
@@ -639,7 +639,7 @@ Proof.
   
   (* inductive case *)
   simpl in H1. inv H1. simpl.
-  destruct (VSet.mem id cenv) as []_eqn. simpl.
+  destruct (VSet.mem id cenv) eqn:?. simpl.
   (* variable is lifted out of memory *)
   exploit Mem.alloc_left_unmapped_inject; eauto. 
   intros [j1 [A [B [C D]]]].
@@ -782,7 +782,7 @@ Proof.
   assert (forall id l1 l2,
           (In id (var_names l1) -> In id (var_names l2)) ->
           (create_undef_temps l1)!id = None \/ (create_undef_temps l1)!id = (create_undef_temps l2)!id).
-    intros. destruct ((create_undef_temps l1)!id) as [v1|]_eqn; auto.
+    intros. destruct ((create_undef_temps l1)!id) as [v1|] eqn:?; auto.
     exploit create_undef_temps_inv; eauto. intros [A B]. subst v1.
     exploit list_in_map_inv. unfold var_names in H. apply H. eexact B.
     intros [[id1 ty1] [P Q]]. simpl in P; subst id1.
@@ -813,7 +813,7 @@ Remark filter_charact:
   In x (List.filter f l) <-> In x l /\ f x = true.
 Proof.
   induction l; simpl. tauto. 
-  destruct (f a) as []_eqn. 
+  destruct (f a) eqn:?. 
   simpl. rewrite IHl. intuition congruence.
   intuition congruence.
 Qed.
@@ -902,7 +902,7 @@ Proof.
   unfold var_names in i. exploit list_in_map_inv; eauto.
   intros [[id' ty] [EQ IN]]; simpl in EQ; subst id'.
   exploit F; eauto. intros [b [P R]]. 
-  destruct (VSet.mem id cenv) as []_eqn.
+  destruct (VSet.mem id cenv) eqn:?.
   (* local var, lifted *)
   destruct R as [U V]. exploit H2; eauto. intros [chunk X]. 
   eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto.
@@ -918,7 +918,7 @@ Proof.
   (* non-local var *)
   exploit G; eauto. unfold empty_env. rewrite PTree.gempty. intros [U V].
   eapply match_var_not_local; eauto. 
-  destruct (VSet.mem id cenv) as []_eqn; auto.
+  destruct (VSet.mem id cenv) eqn:?; auto.
   elim n; eauto.
 
   (* temps *)
@@ -1072,7 +1072,7 @@ Proof.
   (* inductive case *)
   inv NOREPET. inv CASTED. inv VINJ.
   exploit me_vars; eauto. instantiate (1 := id); intros MV.
-  destruct (VSet.mem id cenv) as []_eqn.
+  destruct (VSet.mem id cenv) eqn:?.
   (* lifted to temp *)
   eapply IHbind_parameters with (tle1 := PTree.set id v' tle1); eauto.
   eapply match_envs_assign_lifted; eauto. 
@@ -1164,7 +1164,7 @@ Proof.
   induction l; simpl; intros.
   contradiction.
   destruct a as [[b1 lo1] hi1]. 
-  destruct (Mem.free m b1 lo1 hi1) as [m1|]_eqn; try discriminate.
+  destruct (Mem.free m b1 lo1 hi1) as [m1|] eqn:?; try discriminate.
   destruct H0. inv H0. eapply Mem.free_range_perm; eauto. 
   red; intros. eapply Mem.perm_free_3; eauto. eapply IHl; eauto. 
 Qed.
@@ -1209,7 +1209,7 @@ Lemma free_list_right_inject:
 Proof.
   induction l; simpl; intros.
   congruence.
-  destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|]_eqn; try discriminate.
+  destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|] eqn:?; try discriminate.
   eapply IHl with (m2 := m21); eauto.
   eapply Mem.free_right_inject; eauto. 
 Qed.
@@ -1380,8 +1380,8 @@ Proof.
   destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
   destruct (Int.eq i Int.zero); try discriminate; auto.
   destruct (Int.eq i Int.zero); try discriminate; auto.
-  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; try discriminate.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; try discriminate.
+  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
   simpl in H3.
   rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb).
   rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0).
@@ -1509,7 +1509,7 @@ Proof.
 (* addrof *)
   exploit eval_simpl_lvalue; eauto. 
   destruct a; auto with compat.
-  destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. 
+  destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. 
   elim (H0 i). apply VSet.singleton_2. auto. apply VSet.mem_2. auto.
   intros [b' [ofs' [A B]]]. 
   exists (Vptr b' ofs'); split; auto. constructor; auto. 
@@ -1529,7 +1529,7 @@ Proof.
 (* rval *)
   assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true)
                \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)).
-    destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. left; exists i; exists t; auto.  
+    destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. left; exists i; exists t; auto.  
   destruct EITHER as [ [id [ty [EQ OPT]]] | NONOPT ].
   (* a variable pulled out of memory *)
   subst a. simpl. rewrite OPT.
@@ -1696,10 +1696,10 @@ Lemma match_cont_extcall:
 Proof.
   intros. eapply match_cont_invariant; eauto. 
   destruct H0. intros. eapply H5; eauto. 
-  red in H2. intros. destruct (f b) as [[b' delta] | ]_eqn. auto. 
-  destruct (f' b) as [[b' delta] | ]_eqn; auto. 
+  red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto. 
+  destruct (f' b) as [[b' delta] | ] eqn:?; auto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction.
-  red in H2. intros. destruct (f b) as [[b'' delta''] | ]_eqn. auto. 
+  red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction.
 Qed.
 
@@ -1752,7 +1752,7 @@ Remark free_list_nextblock:
 Proof.
   induction l; simpl; intros.
   congruence.
-  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate.
+  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
   transitivity (Mem.nextblock m1). eauto. eapply Mem.nextblock_free; eauto. 
 Qed.
 
@@ -1764,7 +1764,7 @@ Remark free_list_load:
 Proof.
   induction l; simpl; intros.
   inv H; auto.
-  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate.
+  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
   transitivity (Mem.load chunk m1 b' 0). eauto. 
   eapply Mem.load_free. eauto. left. assert (b' < b) by eauto. unfold block; omega.
 Qed.
@@ -1860,7 +1860,7 @@ Remark is_liftable_var_charact:
   end.
 Proof.
   intros. destruct a; simpl; auto.
-  destruct (VSet.mem i cenv) as []_eqn. 
+  destruct (VSet.mem i cenv) eqn:?. 
   exists t; auto. 
   auto.
 Qed.
@@ -2202,7 +2202,7 @@ Proof.
     apply val_list_inject_incr with j'; eauto. 
     eexact B. eexact C.
     intros. apply (create_undef_temps_lifted id f). auto.
-    intros. destruct (create_undef_temps (fn_temps f))!id as [v|]_eqn; auto.
+    intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto.
     exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto.
   intros [tel [tm1 [P [Q [R [S T]]]]]].
   change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f))