Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Val.lessdef, etc.

18 files changed, 373 insertions, 371 deletions

diff --git a/arm/Op.v b/arm/Op.v
index bbdcd123..b5ea9a7a 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -808,40 +808,40 @@ Hypothesis valid_different_pointers_inj:
 
 Ltac InvInject :=
   match goal with
-  | [ H: val_inject _ (Vint _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vint _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vfloat _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vsingle _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vsingle _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vptr _ _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ nil _ |- _ ] =>
+  | [ H: Val.inject_list _ nil _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ (_ :: _) _ |- _ ] =>
+  | [ H: Val.inject_list _ (_ :: _) _ |- _ ] =>
       inv H; InvInject
   | _ => idtac
   end.
 
 Remark eval_shift_inj:
-  forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v').
+  forall s v v', Val.inject f v v' -> Val.inject f (eval_shift s v) (eval_shift s v').
 Proof.
   intros. inv H; destruct s; simpl; auto; rewrite s_range; auto. 
 Qed.
 
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl.
-  eauto 4 using val_cmp_bool_inject.
-  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
-  eauto using val_cmp_bool_inject, eval_shift_inj.
-  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj.
-  eauto 4 using val_cmp_bool_inject.
-  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto 4 using Val.cmp_bool_inject.
+  eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto using Val.cmp_bool_inject, eval_shift_inj.
+  eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj.
+  eauto 4 using Val.cmp_bool_inject.
+  eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; simpl in H0; inv H0; auto.
@@ -854,7 +854,7 @@ Qed.
 
 Ltac TrivialExists :=
   match goal with
-  | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
+  | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
       exists v1; split; auto
   | _ => idtac
   end.
@@ -863,28 +863,28 @@ Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_operation op) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
-  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
-  apply Values.val_add_inject; auto.
+  apply Values.Val.add_inject; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
-  apply Values.val_add_inject; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.Val.add_inject; auto.
 
-  apply Values.val_sub_inject; auto.
-  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
-  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
-  apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto.
+  apply Values.Val.sun_inject; auto.
+  apply Values.Val.sun_inject; auto. apply eval_shift_inj; auto.
+  apply Values.Val.sun_inject; auto. apply eval_shift_inj; auto.
+  apply (@Values.Val.sun_inject f (Vint i) (Vint i) v v'); auto.
 
   inv H4; inv H2; simpl; auto.
-  apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto.
+  apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
@@ -958,17 +958,17 @@ Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_addressing addr) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing ge1 sp1 addr vl1 = Some v1 ->
-  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
-  apply Values.val_add_inject; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.Val.add_inject; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -1034,7 +1034,7 @@ Proof.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
-  rewrite <- val_list_inject_lessdef. eauto. auto.
+  rewrite <- val_inject_list_lessdef. eauto. auto.
 Qed.
 
 Lemma eval_operation_lessdef:
@@ -1044,10 +1044,10 @@ Lemma eval_operation_lessdef:
   eval_operation genv sp op vl1 m1 = Some v1 ->
   exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_operation genv sp op vl2 m2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   apply valid_pointer_extends; auto.
   apply weak_valid_pointer_extends; auto.
@@ -1065,10 +1065,10 @@ Lemma eval_addressing_lessdef:
   eval_addressing genv sp addr vl1 = Some v1 ->
   exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_addressing genv sp addr vl2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_addressing_inj with (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto. 
   rewrite <- val_inject_lessdef; auto. 
@@ -1092,7 +1092,7 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
+  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
@@ -1101,7 +1101,7 @@ Qed.
 
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
@@ -1115,11 +1115,11 @@ Qed.
 
 Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
   exists v2, 
      eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_addressing. simpl.
@@ -1129,12 +1129,12 @@ Qed.
 
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
   exists v2,
      eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_operation. simpl.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index e3c5bf2a..993e0b34 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -109,11 +109,11 @@ Qed.
 (** ** Agreement between register sets before and after inlining. *)
 
 Definition agree_regs (F: meminj) (ctx: context) (rs rs': regset) :=
-  (forall r, Ple r ctx.(mreg) -> val_inject F rs#r rs'#(sreg ctx r))
+  (forall r, Ple r ctx.(mreg) -> Val.inject F rs#r rs'#(sreg ctx r))
 /\(forall r, Plt ctx.(mreg) r -> rs#r = Vundef).
 
 Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: reg) :=
-  (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ val_inject F v rs'#(sreg ctx r)).
+  (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ Val.inject F v rs'#(sreg ctx r)).
 
 Remark Plt_Ple_dec:
   forall p q, {Plt p q} + {Ple q p}.
@@ -138,7 +138,7 @@ Proof.
 Qed.
 
 Lemma agree_val_reg:
-  forall F ctx rs rs' r, agree_regs F ctx rs rs' -> val_inject F rs#r rs'#(sreg ctx r).
+  forall F ctx rs rs' r, agree_regs F ctx rs rs' -> Val.inject F rs#r rs'#(sreg ctx r).
 Proof.
   intros. exploit agree_val_reg_gen; eauto. instantiate (1 := r). intros [[A B] | [A B]].
   rewrite B; auto.
@@ -146,7 +146,7 @@ Proof.
 Qed.
 
 Lemma agree_val_regs:
-  forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> val_list_inject F rs##rl rs'##(sregs ctx rl).
+  forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> Val.inject_list F rs##rl rs'##(sregs ctx rl).
 Proof.
   induction rl; intros; simpl. constructor. constructor; auto. apply agree_val_reg; auto.
 Qed.
@@ -154,7 +154,7 @@ Qed.
 Lemma agree_set_reg:
   forall F ctx rs rs' r v v',
   agree_regs F ctx rs rs' ->
-  val_inject F v v' ->
+  Val.inject F v v' ->
   Ple r ctx.(mreg) ->
   agree_regs F ctx (rs#r <- v) (rs'#(sreg ctx r) <- v').
 Proof.
@@ -218,7 +218,7 @@ Qed.
 
 Lemma agree_regs_init_regs:
   forall F ctx rl vl vl',
-  val_list_inject F vl vl' ->
+  Val.inject_list F vl vl' ->
   (forall r, In r rl -> Ple r ctx.(mreg)) ->
   agree_regs F ctx (init_regs vl rl) (init_regs vl' (sregs ctx rl)).
 Proof.
@@ -389,7 +389,7 @@ Proof.
   (* register *)
   assert (rs'#(sreg ctx r) = rs#r).
     exploit Genv.find_funct_inv; eauto. intros [b EQ].
-    assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
+    assert (A: Val.inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
     rewrite EQ in A; inv A.
     inv H1. rewrite DOMAIN in H5. inv H5. auto.
     apply FUNCTIONS with fd. 
@@ -411,7 +411,7 @@ Lemma tr_annot_arg:
   forall a v,
   eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
   exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v'
-          /\ val_inject F v v'.
+          /\ Val.inject F v v'.
 Proof.
   intros until m'; intros MG AG SP MI. induction 1; simpl.
 - exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto.
@@ -424,7 +424,7 @@ Proof.
   simpl. econstructor; eauto. rewrite Int.add_zero_l; auto.
   intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. 
 - econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto.
-- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
+- assert (Val.inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
   { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
     rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
     inv MG. econstructor. eauto. rewrite Int.add_zero; auto. }
@@ -436,7 +436,7 @@ Proof.
   inv MG. econstructor. eauto. rewrite Int.add_zero; auto.
 - destruct IHeval_annot_arg1 as (v1 & A1 & B1).
   destruct IHeval_annot_arg2 as (v2 & A2 & B2).
-  econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. 
+  econstructor; split. eauto with aarg. apply Val.longofwords_inject; auto. 
 Qed.
 
 Lemma tr_annot_args:
@@ -448,7 +448,7 @@ Lemma tr_annot_args:
   forall al vl,
   eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
   exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl'
-          /\ val_list_inject F vl vl'.
+          /\ Val.inject_list F vl vl'.
 Proof.
   induction 5; simpl.
 - exists (@nil val); split; constructor.
@@ -856,7 +856,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_call_states: forall stk fd args m stk' fd' args' m' F
         (MS: match_stacks F m m' stk stk' (Mem.nextblock m'))
         (FD: transf_fundef fenv fd = OK fd')
-        (VINJ: val_list_inject F args args')
+        (VINJ: Val.inject_list F args args')
         (MINJ: Mem.inject F m m'),
       match_states (Callstate stk fd args m)
                    (Callstate stk' fd' args' m')
@@ -876,7 +876,7 @@ Inductive match_states: state -> state -> Prop :=
                    (State stk' f' (Vptr sp' Int.zero) pc' rs' m')
   | match_return_states: forall stk v m stk' v' m' F
         (MS: match_stacks F m m' stk stk' (Mem.nextblock m'))
-        (VINJ: val_inject F v v')
+        (VINJ: Val.inject F v v')
         (MINJ: Mem.inject F m m'),
       match_states (Returnstate stk v m)
                    (Returnstate stk' v' m')
@@ -884,7 +884,7 @@ Inductive match_states: state -> state -> Prop :=
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
         (RET: ctx.(retinfo) = Some rinfo)
         (AT: f'.(fn_code)!pc' = Some(inline_return ctx or rinfo))
-        (VINJ: match or with None => v = Vundef | Some r => val_inject F v rs'#(sreg ctx r) end)
+        (VINJ: match or with None => v = Vundef | Some r => Val.inject F v rs'#(sreg ctx r) end)
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
@@ -1120,7 +1120,7 @@ Proof.
 
 (* jumptable *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
-  assert (val_inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto.
+  assert (Val.inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto.
   rewrite H0 in H2; inv H2. 
   left; econstructor; split.
   eapply plus_one. eapply exec_Ijumptable; eauto.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 8beff265..770648b1 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -840,7 +840,7 @@ Lemma default_needs_of_condition_sound:
   eval_condition cond args2 m2 = Some b.
 Proof.
   intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto.
-  apply val_list_inject_lessdef. apply lessdef_vagree_list. auto.
+  apply val_inject_list_lessdef. apply lessdef_vagree_list. auto.
 Qed.
 
 Lemma default_needs_of_operation_sound:
@@ -866,7 +866,7 @@ Proof.
   eassumption. auto. auto. auto.
   instantiate (1 := op). intros. apply val_inject_lessdef; auto.
   apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto.
-  apply val_list_inject_lessdef; eauto.
+  apply val_inject_list_lessdef; eauto.
   eauto.
   intros (v2 & A & B). exists v2; split; auto.
   apply vagree_lessdef. apply val_inject_lessdef. auto. 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index f4a1935f..7f41512e 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -508,14 +508,14 @@ Qed.
 (** A variant of [index_contains], up to a memory injection. *)
 
 Definition index_contains_inj (j: meminj) (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop :=
-  exists v', index_contains m sp idx v' /\ val_inject j v v'.
+  exists v', index_contains m sp idx v' /\ Val.inject j v v'.
 
 Lemma gss_index_contains_inj:
   forall j idx m m' sp v v',
   Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' ->
   index_valid idx ->
   Val.has_type v (type_of_index idx) ->
-  val_inject j v v' ->
+  Val.inject j v v' ->
   index_contains_inj j m' sp idx v.
 Proof.
   intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]].
@@ -530,7 +530,7 @@ Lemma gss_index_contains_inj':
   forall j idx m m' sp v v',
   Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' ->
   index_valid idx ->
-  val_inject j v v' ->
+  Val.inject j v v' ->
   index_contains_inj j m' sp idx (Val.load_result (chunk_of_type (type_of_index idx)) v).
 Proof.
   intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]].
@@ -598,7 +598,7 @@ Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking.
 (** Agreement with Mach register states *)
 
 Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop :=
-  forall r, val_inject j (ls (R r)) (rs r).
+  forall r, Val.inject j (ls (R r)) (rs r).
 
 (** Agreement over data stored in memory *)
 
@@ -693,14 +693,14 @@ Definition agree_callee_save (ls ls0: locset) : Prop :=
 
 Lemma agree_reg:
   forall j ls rs r,
-  agree_regs j ls rs -> val_inject j (ls (R r)) (rs r).
+  agree_regs j ls rs -> Val.inject j (ls (R r)) (rs r).
 Proof.
   intros. auto. 
 Qed.
 
 Lemma agree_reglist:
   forall j ls rs rl,
-  agree_regs j ls rs -> val_list_inject j (reglist ls rl) (rs##rl).
+  agree_regs j ls rs -> Val.inject_list j (reglist ls rl) (rs##rl).
 Proof.
   induction rl; simpl; intros.
   auto. constructor. eauto with stacking. auto. 
@@ -713,7 +713,7 @@ Hint Resolve agree_reg agree_reglist: stacking.
 Lemma agree_regs_set_reg:
   forall j ls rs r v v',
   agree_regs j ls rs ->
-  val_inject j v v' ->
+  Val.inject j v v' ->
   agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs).
 Proof.
   intros; red; intros. 
@@ -725,7 +725,7 @@ Qed.
 Lemma agree_regs_set_regs:
   forall j rl vl vl' ls rs,
   agree_regs j ls rs ->
-  val_list_inject j vl vl' ->
+  Val.inject_list j vl vl' ->
   agree_regs j (Locmap.setlist (map R rl) vl ls) (set_regs rl vl' rs).
 Proof.
   induction rl; simpl; intros. 
@@ -850,7 +850,7 @@ Lemma agree_frame_set_local:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
-  val_inject j v v' ->
+  Val.inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
@@ -889,7 +889,7 @@ Lemma agree_frame_set_outgoing:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
-  val_inject j v v' ->
+  Val.inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
@@ -981,7 +981,7 @@ Lemma agree_frame_parallel_stores:
   forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   Mem.inject j m m' ->
-  val_inject j addr addr' ->
+  Val.inject j addr addr' ->
   Mem.storev chunk m addr v = Some m1 ->
   Mem.storev chunk m' addr' v' = Some m1' ->
   agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
@@ -1669,7 +1669,7 @@ Hypothesis mkindex_val:
   index_contains_inj j m sp (mkindex (number r)) (ls0 (R r)).
 
 Definition agree_unused (ls0: locset) (rs: regset) : Prop :=
-  forall r, ~(mreg_within_bounds b r) -> val_inject j (ls0 (R r)) (rs r).
+  forall r, ~(mreg_within_bounds b r) -> Val.inject j (ls0 (R r)) (rs r).
 
 Lemma restore_callee_save_regs_correct:
   forall l rs k,
@@ -1681,7 +1681,7 @@ Lemma restore_callee_save_regs_correct:
       (State cs fb (Vptr sp Int.zero)
         (restore_callee_save_regs bound number mkindex ty fe l k) rs m)
    E0 (State cs fb (Vptr sp Int.zero) k rs' m)
-  /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r))
+  /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r))
   /\ (forall r, ~(In r l) -> rs' r = rs r)
   /\ agree_unused ls0 rs'.
 Proof.
@@ -1734,7 +1734,7 @@ Lemma restore_callee_save_correct:
     E0 (State cs fb (Vptr sp' Int.zero) k rs' m')
   /\ (forall r, 
         In r int_callee_save_regs \/ In r float_callee_save_regs -> 
-        val_inject j (ls0 (R r)) (rs' r))
+        Val.inject j (ls0 (R r)) (rs' r))
   /\ (forall r, 
         ~(In r int_callee_save_regs) ->
         ~(In r float_callee_save_regs) ->
@@ -1986,7 +1986,7 @@ Qed.
 Lemma match_stacks_parallel_stores:
   forall j m m' chunk addr addr' v v' m1 m1',
   Mem.inject j m m' ->
-  val_inject j addr addr' ->
+  Val.inject j addr addr' ->
   Mem.storev chunk m addr v = Some m1 ->
   Mem.storev chunk m' addr' v' = Some m1' ->
   forall cs cs' sg bound bound',
@@ -2327,7 +2327,7 @@ Hypothesis AGCS: agree_callee_save ls (parent_locset cs).
 Lemma transl_external_argument:
   forall l,
   In l (loc_arguments sg) ->
-  exists v, extcall_arg rs m' (parent_sp cs') l v /\ val_inject j (ls l) v.
+  exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v.
 Proof.
   intros.
   assert (loc_argument_acceptable l). apply loc_arguments_acceptable with sg; auto.
@@ -2354,7 +2354,7 @@ Lemma transl_external_arguments_rec:
   forall locs,
   incl locs (loc_arguments sg) ->
   exists vl,
-  list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ val_list_inject j ls##locs vl.
+  list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ Val.inject_list j ls##locs vl.
 Proof.
   induction locs; simpl; intros.
   exists (@nil val); split. constructor. constructor.
@@ -2366,7 +2366,7 @@ Qed.
 Lemma transl_external_arguments:
   exists vl,
   extcall_arguments rs m' (parent_sp cs') sg vl /\
-  val_list_inject j (ls ## (loc_arguments sg)) vl.
+  Val.inject_list j (ls ## (loc_arguments sg)) vl.
 Proof.
   unfold extcall_arguments. 
   apply transl_external_arguments_rec.
@@ -2402,7 +2402,7 @@ Lemma transl_annot_arg_correct:
   (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) ->
   exists v',
      eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v'
-  /\ val_inject j v v'.
+  /\ Val.inject j v v'.
 Proof.
 Local Opaque fe offset_of_index.
   induction 1; simpl; intros VALID BOUNDS.
@@ -2424,7 +2424,7 @@ Local Transparent fe.
   eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. 
 - econstructor; split; eauto with aarg.
   unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto.
-- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
+- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
   { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
     destruct (Genv.find_symbol ge id) eqn:FS; auto.
     econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. }
@@ -2436,7 +2436,7 @@ Local Transparent fe.
 - destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app.
   destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app.
   exists (Val.longofwords v1 v2); split; auto with aarg. 
-  apply val_longofwords_inject; auto. 
+  apply Val.longofwords_inject; auto. 
 Qed.
 
 Lemma transl_annot_args_correct:
@@ -2446,7 +2446,7 @@ Lemma transl_annot_args_correct:
   (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) ->
   exists vl',
      eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl'
-  /\ val_list_inject j vl vl'.
+  /\ Val.inject_list j vl vl'.
 Proof.
   induction 1; simpl; intros VALID BOUNDS.
 - exists (@nil val); split; constructor.
@@ -2618,7 +2618,7 @@ Proof.
 - (* Lop *)
   assert (exists v',
           eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
-       /\ val_inject j v v').
+       /\ Val.inject j v v').
   eapply eval_operation_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
   eapply agree_inj; eauto. eapply agree_reglist; eauto.
@@ -2636,7 +2636,7 @@ Proof.
 - (* Lload *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
-       /\ val_inject j a a').
+       /\ Val.inject j a a').
   eapply eval_addressing_inject; eauto. 
   eapply match_stacks_preserves_globals; eauto.
   eapply agree_inj; eauto. eapply agree_reglist; eauto.
@@ -2654,7 +2654,7 @@ Proof.
 - (* Lstore *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
-       /\ val_inject j a a').
+       /\ Val.inject j a a').
   eapply eval_addressing_inject; eauto. 
   eapply match_stacks_preserves_globals; eauto.
   eapply agree_inj; eauto. eapply agree_reglist; eauto.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 90d7f270..85e7a360 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -554,7 +554,7 @@ Qed.
 Lemma symbol_address_inject:
   forall j id ofs, 
   meminj_preserves_globals j -> kept id ->
-  val_inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).
+  Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
   exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. 
@@ -564,17 +564,17 @@ Qed.
 (** Semantic preservation *)
 
 Definition regset_inject (f: meminj) (rs rs': regset): Prop :=
-  forall r, val_inject f rs#r rs'#r.
+  forall r, Val.inject f rs#r rs'#r.
 
 Lemma regs_inject:
-  forall f rs rs', regset_inject f rs rs' -> forall l, val_list_inject f rs##l rs'##l.
+  forall f rs rs', regset_inject f rs rs' -> forall l, Val.inject_list f rs##l rs'##l.
 Proof.
   induction l; simpl. constructor. constructor; auto. 
 Qed.
 
 Lemma set_reg_inject:
   forall f rs rs' r v v',
-  regset_inject f rs rs' -> val_inject f v v' ->
+  regset_inject f rs rs' -> Val.inject f v v' ->
   regset_inject f (rs#r <- v) (rs'#r <- v').
 Proof.
   intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. 
@@ -593,7 +593,7 @@ Proof.
 Qed.
 
 Lemma init_regs_inject:
-  forall f args args', val_list_inject f args args' ->
+  forall f args args', Val.inject_list f args args' ->
   forall params,
   regset_inject f (init_regs args params) (init_regs args' params).
 Proof.
@@ -689,13 +689,13 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_call: forall s fd args m ts targs tm j
          (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
          (KEPT: forall id, ref_fundef fd id -> kept id)
-         (ARGINJ: val_list_inject j args targs)
+         (ARGINJ: Val.inject_list j args targs)
          (MEMINJ: Mem.inject j m tm),
       match_states (Callstate s fd args m)
                    (Callstate ts fd targs tm)
   | match_states_return: forall s res m ts tres tm j
          (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
-         (RESINJ: val_inject j res tres)
+         (RESINJ: Val.inject j res tres)
          (MEMINJ: Mem.inject j m tm),
       match_states (Returnstate s res m)
                    (Returnstate ts tres tm).
@@ -706,10 +706,10 @@ Lemma external_call_inject:
   external_call ef ge vargs m1 t vres m2 ->
   (forall id, In id (globals_external ef) -> kept id) ->
   Mem.inject f m1 m1' ->
-  val_list_inject f vargs vargs' ->
+  Val.inject_list f vargs vargs' ->
   exists f', exists vres', exists m2',
     external_call ef tge vargs' m1' t vres' m2'
-    /\ val_inject f' vres vres'
+    /\ Val.inject f' vres vres'
     /\ Mem.inject f' m2 m2'
     /\ Mem.unchanged_on (loc_unmapped f) m1 m2
     /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
@@ -751,7 +751,7 @@ Lemma eval_annot_arg_inject:
   (forall id, In id (globals_of_annot_arg a) -> kept id) ->
   exists v',
      eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v'
-  /\ val_inject j v v'.
+  /\ Val.inject j v v'.
 Proof.
   induction 1; intros SP GL RS MI K; simpl in K.
 - exists rs'#x; split; auto. constructor. 
@@ -762,7 +762,7 @@ Proof.
 - simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. 
   intros (v' & A & B). exists v'; auto with aarg.
 - econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto.
-- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
+- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
   { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
     exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. 
@@ -776,7 +776,7 @@ Proof.
 - destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app.
   destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app.
   exists (Val.longofwords v1' v2'); split; auto with aarg. 
-  apply val_longofwords_inject; auto.
+  apply Val.longofwords_inject; auto.
 Qed.
 
 Lemma eval_annot_args_inject:
@@ -789,7 +789,7 @@ Lemma eval_annot_args_inject:
   (forall id, In id (globals_of_annot_args al) -> kept id) ->
   exists vl',
      eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl'
-  /\ val_list_inject j vl vl'.
+  /\ Val.inject_list j vl vl'.
 Proof.
   induction 1; intros. 
 - exists (@nil val); split; constructor.
@@ -814,7 +814,7 @@ Proof.
 - (* op *)
   assert (A: exists tv, 
                eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv
-            /\ val_inject j v tv).
+            /\ Val.inject j v tv).
   { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
     intros; eapply Mem.valid_pointer_inject_val; eauto.
     intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
@@ -832,7 +832,7 @@ Proof.
 - (* load *)
   assert (A: exists ta, 
                eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
-            /\ val_inject j a ta).
+            /\ Val.inject j a ta).
   { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
     intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
     apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto.
@@ -847,7 +847,7 @@ Proof.
 - (* store *)
   assert (A: exists ta, 
                eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
-            /\ val_inject j a ta).
+            /\ Val.inject j a ta).
   { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
     intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
     apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto.
@@ -961,7 +961,7 @@ Proof.
   econstructor; split. 
   eapply exec_function_internal; eauto.
   eapply match_states_regular with (j := j'); eauto.
-  apply init_regs_inject; auto. apply val_list_inject_incr with j; auto. 
+  apply init_regs_inject; auto. apply val_inject_list_incr with j; auto. 
 
 - (* external function *)
   exploit external_call_inject; eauto. 
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 8720ce50..28934ce9 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -923,7 +923,7 @@ Proof.
     rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. 
     rewrite H; congruence.
   }
-  assert (VMTOP: forall v v', val_inject j' v v' -> vmatch bc' v Vtop).
+  assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop).
   {
     intros. inv H; constructor. eapply PMTOP; eauto. 
   }
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index ff3ccfa1..b4c1df61 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -3690,7 +3690,7 @@ Proof.
 Qed.
 
 Lemma vmatch_inj:
-  forall bc v x, vmatch bc v x -> val_inject (inj_of_bc bc) v v.
+  forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v.
 Proof.
   induction 1; econstructor. 
   eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. 
@@ -3698,7 +3698,7 @@ Proof.
 Qed.
 
 Lemma vmatch_list_inj:
-  forall bc vl xl, list_forall2 (vmatch bc) vl xl -> val_list_inject (inj_of_bc bc) vl vl.
+  forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl.
 Proof.
   induction 1; constructor. eapply vmatch_inj; eauto. auto. 
 Qed. 
@@ -3761,7 +3761,7 @@ Proof.
 Qed.
 
 Lemma vmatch_inj_top:
-  forall bc v v', val_inject (inj_of_bc bc) v v' -> vmatch bc v Vtop.
+  forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop.
 Proof.
   intros. inv H; constructor. eapply pmatch_inj_top; eauto. 
 Qed.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 17c59b97..dfc69412 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -163,7 +163,7 @@ Qed.
   [f b = Some(b', ofs)] means that C#minor block [b] corresponds
   to a sub-block of Cminor block [b] at offset [ofs].
 
-  A memory injection [f] defines a relation [val_inject f] between
+  A memory injection [f] defines a relation [Val.inject f] between
   values and a relation [Mem.inject f] between memory states.  These
   relations will be used intensively in our proof of simulation
   between C#minor and Cminor executions. *)
@@ -171,7 +171,7 @@ Qed.
 (** ** Matching between Cshaprminor's temporaries and Cminor's variables *)
 
 Definition match_temps (f: meminj) (le: Csharpminor.temp_env) (te: env) : Prop :=
-  forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ val_inject f v v'.
+  forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ Val.inject f v v'.
 
 Lemma match_temps_invariant:
   forall f f' le te,
@@ -185,7 +185,7 @@ Qed.
 Lemma match_temps_assign:
   forall f le te id v tv,
   match_temps f le te ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   match_temps f (PTree.set id v le) (PTree.set id tv te).
 Proof.
   intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id).
@@ -197,7 +197,7 @@ Qed.
 
 Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop :=
   | match_var_local: forall b sz ofs,
-      val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) ->
+      Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) ->
       match_var f sp (Some(b, sz)) (Some ofs)
   | match_var_global:
       match_var f sp None None.
@@ -553,7 +553,7 @@ Qed.
 
 Lemma match_callstack_set_temp:
   forall f cenv e le te sp lo hi cs bound tbound m tm tf id v tv,
-  val_inject f v tv ->
+  Val.inject f v tv ->
   match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound ->
   match_callstack f m tm (Frame cenv tf e (PTree.set id v le) (PTree.set id tv te) sp lo hi :: cs) bound tbound.
 Proof.
@@ -1119,7 +1119,7 @@ Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.e
 Lemma bind_parameters_agree_rec:
   forall f vars vals tvals le1 le2 te,
   bind_parameters vars vals le1 = Some le2 ->
-  val_list_inject f vals tvals ->
+  Val.inject_list f vals tvals ->
   match_temps f le1 te ->
   match_temps f le2 (set_params' tvals vars te).
 Proof.
@@ -1213,7 +1213,7 @@ Qed.
 Lemma bind_parameters_agree:
   forall f params temps vals tvals le,
   bind_parameters params vals (create_undef_temps temps) = Some le ->
-  val_list_inject f vals tvals ->
+  Val.inject_list f vals tvals ->
   list_norepet params ->
   list_disjoint params temps ->
   match_temps f le (set_locals temps (set_params tvals params)).
@@ -1238,7 +1238,7 @@ Theorem match_callstack_function_entry:
   list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) ->
   alloc_variables Csharpminor.empty_env m (Csharpminor.fn_vars fn) e m' ->
   bind_parameters (Csharpminor.fn_params fn) args (create_undef_temps fn.(fn_temps)) = Some le ->
-  val_list_inject f args targs ->
+  Val.inject_list f args targs ->
   Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
   match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
   Mem.inject f m tm ->
@@ -1259,39 +1259,39 @@ Qed.
 (** * Compatibility of evaluation functions with respect to memory injections. *)
 
 Remark val_inject_val_of_bool:
-  forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
+  forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b).
 Proof.
   intros; destruct b; constructor.
 Qed.
 
 Remark val_inject_val_of_optbool:
-  forall f ob, val_inject f (Val.of_optbool ob) (Val.of_optbool ob).
+  forall f ob, Val.inject f (Val.of_optbool ob) (Val.of_optbool ob).
 Proof.
   intros; destruct ob; simpl. destruct b; constructor. constructor.
 Qed.
 
 Ltac TrivialExists :=
   match goal with
-  | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] =>
+  | [ |- exists y, Some ?x = Some y /\ Val.inject _ _ _ ] =>
       exists x; split; [auto | try(econstructor; eauto)]
-  | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] =>
+  | [ |- exists y, _ /\ Val.inject _ (Vint ?x) _ ] =>
       exists (Vint x); split; [eauto with evalexpr | constructor]
-  | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] =>
+  | [ |- exists y, _ /\ Val.inject _ (Vfloat ?x) _ ] =>
       exists (Vfloat x); split; [eauto with evalexpr | constructor]
-  | [ |- exists y, _ /\ val_inject _ (Vlong ?x) _ ] =>
+  | [ |- exists y, _ /\ Val.inject _ (Vlong ?x) _ ] =>
       exists (Vlong x); split; [eauto with evalexpr | constructor]
   | _ => idtac
   end.
 
-(** Compatibility of [eval_unop] with respect to [val_inject]. *)
+(** Compatibility of [eval_unop] with respect to [Val.inject]. *)
 
 Lemma eval_unop_compat:
   forall f op v1 tv1 v,
   eval_unop op v1 = Some v ->
-  val_inject f v1 tv1 ->
+  Val.inject f v1 tv1 ->
   exists tv,
      eval_unop op tv1 = Some tv
-  /\ val_inject f v tv.
+  /\ Val.inject f v tv.
 Proof.
   destruct op; simpl; intros.
   inv H; inv H0; simpl; TrivialExists.
@@ -1329,17 +1329,17 @@ Proof.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
 Qed.
 
-(** Compatibility of [eval_binop] with respect to [val_inject]. *)
+(** Compatibility of [eval_binop] with respect to [Val.inject]. *)
 
 Lemma eval_binop_compat:
   forall f op v1 tv1 v2 tv2 v m tm,
   eval_binop op v1 v2 m = Some v ->
-  val_inject f v1 tv1 ->
-  val_inject f v2 tv2 ->
+  Val.inject f v1 tv1 ->
+  Val.inject f v2 tv2 ->
   Mem.inject f m tm ->
   exists tv,
      eval_binop op tv1 tv2 tm = Some tv
-  /\ val_inject f v tv.
+  /\ Val.inject f v tv.
 Proof.
   destruct op; simpl; intros.
   inv H; inv H0; inv H1; TrivialExists.
@@ -1401,7 +1401,7 @@ Proof.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
   replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
   destruct b; simpl; constructor.
-  symmetry. eapply val_cmpu_bool_inject; eauto.
+  symmetry. eapply Val.cmpu_bool_inject; eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
@@ -1429,7 +1429,7 @@ Lemma var_addr_correct:
   eval_var_addr ge e id b ->
   exists tv,
      eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv
-  /\ val_inject f (Vptr b Int.zero) tv.
+  /\ Val.inject f (Vptr b Int.zero) tv.
 Proof.
   unfold var_addr; intros.
   assert (match_var f sp e!id cenv!id).
@@ -1474,7 +1474,7 @@ Qed.
 
 Remark bool_of_val_inject:
   forall f v tv b,
-  Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b.
+  Val.bool_of_val v b -> Val.inject f v tv -> Val.bool_of_val tv b.
 Proof.
   intros. inv H0; inv H; constructor; auto.
 Qed.
@@ -1484,7 +1484,7 @@ Lemma transl_constant_correct:
   Csharpminor.eval_constant cst = Some v ->
   exists tv,
      eval_constant tge sp (transl_constant cst) = Some tv
-  /\ val_inject f v tv.
+  /\ Val.inject f v tv.
 Proof.
   destruct cst; simpl; intros; inv H. 
   exists (Vint i); auto.
@@ -1505,7 +1505,7 @@ Lemma transl_expr_correct:
     (TR: transl_expr cenv a = OK ta),
   exists tv,
      eval_expr tge (Vptr sp Int.zero) te tm ta tv
-  /\ val_inject f v tv.
+  /\ Val.inject f v tv.
 Proof.
   induction 3; intros; simpl in TR; try (monadInv TR).
   (* Etempvar *)
@@ -1543,7 +1543,7 @@ Lemma transl_exprlist_correct:
     (TR: transl_exprlist cenv a = OK ta),
   exists tv,
      eval_exprlist tge (Vptr sp Int.zero) te tm ta tv
-  /\ val_list_inject f v tv.
+  /\ Val.inject_list f v tv.
 Proof.
   induction 3; intros; monadInv TR.
   exists (@nil val); split. constructor. constructor.
@@ -1610,7 +1610,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
       (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
       (MK: match_cont k tk cenv nil cs)
       (ISCC: Csharpminor.is_call_cont k)
-      (ARGSINJ: val_list_inject f args targs),
+      (ARGSINJ: Val.inject_list f args targs),
       match_states (Csharpminor.Callstate fd args k m)
                    (Callstate tfd targs tk tm)
   | match_returnstate:
@@ -1618,7 +1618,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
       (MINJ: Mem.inject f m tm)
       (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
       (MK: match_cont k tk cenv nil cs)
-      (RESINJ: val_inject f v tv),
+      (RESINJ: Val.inject f v tv),
       match_states (Csharpminor.Returnstate v k m)
                    (Returnstate tv tk tm).
 
@@ -1626,7 +1626,7 @@ Remark val_inject_function_pointer:
   forall bound v fd f tv,
   Genv.find_funct ge v = Some fd ->
   match_globalenvs f bound ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   tv = v.
 Proof.
   intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 2a5d17bc..6284660c 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -1054,13 +1054,13 @@ Hypothesis valid_different_pointers_inj:
   b1' <> b2' \/
   Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 
-Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue.
+Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue.
 Proof. unfold Vtrue; auto. Qed.
 
-Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse.
+Remark val_inject_vfalse: forall f, Val.inject f Vfalse Vfalse.
 Proof. unfold Vfalse; auto. Qed.
 
-Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
+Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b).
 Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. 
 Qed.
 
@@ -1075,8 +1075,8 @@ Ltac TrivialInject :=
 Lemma sem_cast_inject:
   forall v1 ty1 ty v tv1,
   sem_cast v1 ty1 ty = Some v ->
-  val_inject f v1 tv1 ->
-  exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv.
+  Val.inject f v1 tv1 ->
+  exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_cast; intros; destruct (classify_cast ty1 ty);
   inv H0; inv H; TrivialInject.
@@ -1093,8 +1093,8 @@ Qed.
 Lemma sem_unary_operation_inj:
   forall op v1 ty v tv1,
   sem_unary_operation op v1 ty m = Some v ->
-  val_inject f v1 tv1 ->
-  exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv.
+  Val.inject f v1 tv1 ->
+  exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_unary_operation; intros. destruct op.
   (* notbool *)
@@ -1118,15 +1118,15 @@ Definition optval_self_injects (ov: option val) : Prop :=
 Remark sem_binarith_inject:
   forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2',
   sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v ->
-  val_inject f v1 v1' -> val_inject f v2 v2' ->
+  Val.inject f v1 v1' -> Val.inject f v2 v2' ->
   (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) ->
   (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_float n1 n2)) ->
   (forall n1 n2, optval_self_injects (sem_single n1 n2)) ->
-  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'.
+  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'.
 Proof.
   intros. 
-  assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v).
+  assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v).
   {
     intros. subst ov; simpl in H7. destruct v0; contradiction || constructor.
   }
@@ -1144,8 +1144,8 @@ Qed.
 Remark sem_shift_inject:
   forall sem_int sem_long v1 t1 v2 t2 v v1' v2',
   sem_shift sem_int sem_long v1 t1 v2 t2 = Some v ->
-  val_inject f v1 v1' -> val_inject f v2 v2' ->
-  exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'.
+  Val.inject f v1 v1' -> Val.inject f v2 v2' ->
+  exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.inject f v v'.
 Proof.
   intros. exists v.
   unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate.
@@ -1158,9 +1158,9 @@ Qed.
 Remark sem_cmp_inj:
   forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
   sem_cmp cmp v1 ty1 v2 ty2 m = Some v ->
-  val_inject f v1 tv1 ->
-  val_inject f v2 tv2 ->
-  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+  Val.inject f v1 tv1 ->
+  Val.inject f v2 tv2 ->
+  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.
 Proof.
   intros.
   unfold sem_cmp in *; destruct (classify_cmp ty1 ty2).
@@ -1168,21 +1168,21 @@ Proof.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
   replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b).
   simpl. TrivialInject. 
-  symmetry. eapply val_cmpu_bool_inject; eauto. 
+  symmetry. eapply Val.cmpu_bool_inject; eauto. 
 - (* pointer - long *)
   destruct v2; try discriminate. inv H1. 
   set (v2 := Vint (Int.repr (Int64.unsigned i))) in *.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
   replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b).
   simpl. TrivialInject. 
-  symmetry. eapply val_cmpu_bool_inject with (v2 := v2); eauto. constructor. 
+  symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. 
 - (* long - pointer *)
   destruct v1; try discriminate. inv H0. 
   set (v1 := Vint (Int.repr (Int64.unsigned i))) in *.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
   replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b).
   simpl. TrivialInject. 
-  symmetry. eapply val_cmpu_bool_inject with (v1 := v1); eauto. constructor. 
+  symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. 
 - (* numerical - numerical *)
   assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))).
   {
@@ -1194,8 +1194,8 @@ Qed.
 Lemma sem_binary_operation_inj:
   forall cenv op v1 ty1 v2 ty2 v tv1 tv2,
   sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
-  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
-  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+  Val.inject f v1 tv1 -> Val.inject f v2 tv2 ->
+  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_binary_operation; intros; destruct op.
 - (* add *)
@@ -1269,7 +1269,7 @@ Qed.
 Lemma bool_val_inj:
   forall v ty b tv,
   bool_val v ty m = Some b ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   bool_val tv ty m' = Some b.
 Proof.
   unfold bool_val; intros. 
@@ -1283,9 +1283,9 @@ End GENERIC_INJECTION.
 Lemma sem_unary_operation_inject:
   forall f m m' op v1 ty1 v tv1,
   sem_unary_operation op v1 ty1 m = Some v ->
-  val_inject f v1 tv1 ->
+  Val.inject f v1 tv1 ->
   Mem.inject f m m' ->
-  exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv.
+  exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ Val.inject f v tv.
 Proof.
   intros. eapply sem_unary_operation_inj; eauto. 
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
@@ -1294,9 +1294,9 @@ Qed.
 Lemma sem_binary_operation_inject:
   forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2,
   sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
-  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
+  Val.inject f v1 tv1 -> Val.inject f v2 tv2 ->
   Mem.inject f m m' ->
-  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.
 Proof.
   intros. eapply sem_binary_operation_inj; eauto. 
   intros; eapply Mem.valid_pointer_inject_val; eauto.
@@ -1308,7 +1308,7 @@ Qed.
 Lemma bool_val_inject:
   forall f m m' v ty b tv,
   bool_val v ty m = Some b ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   Mem.inject f m m' ->
   bool_val tv ty m' = Some b.
 Proof.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index e0fcb210..790877bd 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -358,8 +358,8 @@ Lemma sem_cast_match:
   forall v1 ty1 ty2 v2 v1' v2',
   sem_cast v1 ty1 ty2 = Some v2 ->
   do_cast v1' ty1 ty2 = OK v2' ->
-  val_inject inj v1' v1 ->
-  val_inject inj v2' v2.
+  Val.inject inj v1' v1 ->
+  Val.inject inj v2' v2.
 Proof.
   intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0.
   exploit sem_cast_inject. eexact E. eauto. 
@@ -369,7 +369,7 @@ Qed.
 Lemma bool_val_match:
   forall v ty b v' m,
   bool_val v ty Mem.empty = Some b ->
-  val_inject inj v v' ->
+  Val.inject inj v v' ->
   bool_val v' ty m = Some b.
 Proof.
   intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate.
@@ -382,13 +382,13 @@ Lemma constval_rvalue:
   eval_simple_rvalue empty_env m a v ->
   forall v',
   constval ge a = OK v' ->
-  val_inject inj v' v
+  Val.inject inj v' v
 with constval_lvalue:
   forall m a b ofs,
   eval_simple_lvalue empty_env m a b ofs ->
   forall v',
   constval ge a = OK v' ->
-  val_inject inj v' (Vptr b ofs).
+  Val.inject inj v' (Vptr b ofs).
 Proof.
   (* rvalue *)
   induction 1; intros vres CV; simpl in CV; try (monadInv CV).
@@ -479,7 +479,7 @@ Theorem constval_steps:
   forall f r m v v' ty m',
   star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
   constval ge r = OK v ->
-  m' = m /\ ty = typeof r /\ val_inject inj v v'.
+  m' = m /\ ty = typeof r /\ Val.inject inj v v'.
 Proof.
   intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. 
   intros [A [B C]]. intuition. eapply constval_rvalue; eauto.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 3364ec6a..2a50f985 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -107,7 +107,7 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t
       (MODE: access_mode ty = By_value chunk)
       (LOAD: Mem.load chunk m b 0 = Some v)
       (TLENV: tle!(id) = Some tv)
-      (VINJ: val_inject f v tv),
+      (VINJ: Val.inject f v tv),
       match_var f cenv e m te tle id
   | match_var_not_lifted: forall b ty b'
       (ENV: e!id = Some(b, ty))
@@ -130,7 +130,7 @@ Record match_envs (f: meminj) (cenv: compilenv)
     me_temps:
       forall id v,
       le!id = Some v ->
-      (exists tv, tle!id = Some tv /\ val_inject f v tv)
+      (exists tv, tle!id = Some tv /\ Val.inject f v tv)
       /\ (VSet.mem id cenv = true -> v = Vundef);
     me_inj:
       forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2;
@@ -327,7 +327,7 @@ Qed.
 
 Lemma val_casted_inject:
   forall f v v' ty,
-  val_inject f v v' -> val_casted v ty -> val_casted v' ty.
+  Val.inject f v v' -> val_casted v ty -> val_casted v' ty.
 Proof.
   intros. inv H; auto.
   inv H0; constructor.
@@ -383,7 +383,7 @@ Lemma match_envs_assign_lifted:
   match_envs f cenv e le m lo hi te tle tlo thi ->
   e!id = Some(b, ty) ->
   val_casted v ty ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   assign_loc ge ty m b Int.zero v m' ->
   VSet.mem id cenv = true ->
   match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi.
@@ -415,7 +415,7 @@ Qed.
 Lemma match_envs_set_temp:
   forall f cenv e le m lo hi te tle tlo thi id v tv x,
   match_envs f cenv e le m lo hi te tle tlo thi ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   check_temp cenv id = OK x ->
   match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi.
 Proof.
@@ -436,7 +436,7 @@ Qed.
 Lemma match_envs_set_opttemp:
   forall f cenv e le m lo hi te tle tlo thi optid v tv x,
   match_envs f cenv e le m lo hi te tle tlo thi ->
-  val_inject f v tv ->
+  Val.inject f v tv ->
   check_opttemp cenv optid = OK x ->
   match_envs f cenv e (set_opttemp optid v le) m lo hi te (set_opttemp optid tv tle) tlo thi.
 Proof.
@@ -993,8 +993,8 @@ Qed.
 Lemma assign_loc_inject:
   forall f ty m loc ofs v m' tm loc' ofs' v',
   assign_loc ge ty m loc ofs v m' ->
-  val_inject f (Vptr loc ofs) (Vptr loc' ofs') ->
-  val_inject f v v' ->
+  Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
+  Val.inject f v v' ->
   Mem.inject f m tm ->
   exists tm',
      assign_loc tge ty tm loc' ofs' v' tm'
@@ -1095,7 +1095,7 @@ Theorem store_params_correct:
   forall s tm tle1 tle2 targs,
   list_norepet (var_names params) ->
   list_forall2 val_casted args (map snd params) ->
-  val_list_inject j args targs ->
+  Val.inject_list j args targs ->
   match_envs j cenv e le m lo hi te tle1 tlo thi ->
   Mem.inject j m tm ->
   (forall id, ~In id (var_names params) -> tle2!id = tle1!id) ->
@@ -1388,8 +1388,8 @@ Qed.
 Lemma deref_loc_inject:
   forall ty loc ofs v loc' ofs',
   deref_loc ty m loc ofs v ->
-  val_inject f (Vptr loc ofs) (Vptr loc' ofs') ->
-  exists tv, deref_loc ty tm loc' ofs' tv /\ val_inject f v tv.
+  Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
+  exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv.
 Proof.
   intros. inv H. 
   (* by value *)
@@ -1405,14 +1405,14 @@ Lemma eval_simpl_expr:
   forall a v,
   eval_expr ge e le m a v ->
   compat_cenv (addr_taken_expr a) cenv ->
-  exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ val_inject f v tv
+  exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv
 
 with eval_simpl_lvalue:
   forall a b ofs,
   eval_lvalue ge e le m a b ofs ->
   compat_cenv (addr_taken_expr a) cenv ->
   match a with Evar id ty => VSet.mem id cenv = false | _ => True end ->
-  exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ val_inject f (Vptr b ofs) (Vptr b' ofs').
+  exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs').
 
 Proof.
   destruct 1; simpl; intros.
@@ -1512,7 +1512,7 @@ Lemma eval_simpl_exprlist:
   val_casted_list vl tyl /\
   exists tvl,
      eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl
-  /\ val_list_inject f vl tvl.
+  /\ Val.inject_list f vl tvl.
 Proof.
   induction 1; simpl; intros.
   split. constructor. econstructor; split. constructor. auto.
@@ -1729,7 +1729,7 @@ Lemma match_cont_find_funct:
   forall f cenv k tk m bound tbound vf fd tvf,
   match_cont f cenv k tk m bound tbound ->
   Genv.find_funct ge vf = Some fd ->
-  val_inject f vf tvf ->
+  Val.inject f vf tvf ->
   exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd.
 Proof.
   intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG.
@@ -1761,7 +1761,7 @@ Inductive match_states: state -> state -> Prop :=
         (TRFD: transf_fundef fd = OK tfd)
         (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
         (MINJ: Mem.inject j m tm)
-        (AINJ: val_list_inject j vargs tvargs)
+        (AINJ: Val.inject_list j vargs tvargs)
         (FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
         (ANORM: val_casted_list vargs targs),
       match_states (Callstate fd vargs k m)
@@ -1770,7 +1770,7 @@ Inductive match_states: state -> state -> Prop :=
       forall v k m tv tk tm j
         (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
         (MINJ: Mem.inject j m tm)
-        (RINJ: val_inject j v tv),
+        (RINJ: Val.inject j v tv),
       match_states (Returnstate v k m)
                    (Returnstate tv tk tm).
 
@@ -2171,7 +2171,7 @@ Proof.
     eauto. 
     eapply list_norepet_append_left; eauto.
     apply val_casted_list_params. unfold type_of_function in FUNTY. congruence.
-    apply val_list_inject_incr with j'; eauto. 
+    apply val_inject_list_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.
diff --git a/common/Events.v b/common/Events.v
index 3bec15db..78162fff 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -453,7 +453,7 @@ Hypothesis symb_inj: symbols_inject.
 
 Lemma eventval_match_inject:
   forall ev ty v1 v2,
-  eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2.
+  eventval_match ge1 ev ty v1 -> Val.inject f v1 v2 -> eventval_match ge2 ev ty v2.
 Proof.
   intros. inv H; inv H0; try constructor; auto.
   destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ.
@@ -463,7 +463,7 @@ Qed.
 Lemma eventval_match_inject_2:
   forall ev ty v1,
   eventval_match ge1 ev ty v1 -> 
-  exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2.
+  exists v2, eventval_match ge2 ev ty v2 /\ Val.inject f v1 v2.
 Proof.
   intros. inv H; try (econstructor; split; eauto; constructor; fail).
   destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]].
@@ -473,7 +473,7 @@ Qed.
 
 Lemma eventval_list_match_inject:
   forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 ->
-  forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2.
+  forall vl2, Val.inject_list f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2.
 Proof.
   induction 1; intros. inv H; constructor.
   inv H1. constructor. eapply eventval_match_inject; eauto. eauto.
@@ -669,10 +669,10 @@ Record extcall_properties (sem: extcall_sem)
        exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2) ->
     sem ge1 vargs m1 t vres m2 ->
     Mem.inject f m1 m1' ->
-    val_list_inject f vargs vargs' ->
+    Val.inject_list f vargs vargs' ->
     exists f', exists vres', exists m2',
        sem ge2 vargs' m1' t vres' m2'
-    /\ val_inject f' vres vres'
+    /\ Val.inject f' vres vres'
     /\ Mem.inject f' m2 m2'
     /\ Mem.unchanged_on (loc_unmapped f) m1 m2
     /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
@@ -735,9 +735,9 @@ Lemma volatile_load_inject:
   forall ge1 ge2 f chunk m b ofs t v b' ofs' m',
   symbols_inject f ge1 ge2 ->
   volatile_load ge1 chunk m b ofs t v ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   Mem.inject f m m' ->
-  exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'.
+  exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ Val.inject f v v'.
 Proof.
   intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). 
   inv VL.
@@ -747,7 +747,7 @@ Proof.
   rewrite Int.add_zero. exists (Val.load_result chunk v2); split.
   constructor; auto.
   erewrite D; eauto.
-  apply val_load_result_inject. auto.
+  apply Val.load_result_inject. auto.
 - (* normal load *)
   exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). 
   exists v2; split; auto. 
@@ -852,7 +852,7 @@ Proof.
 (* inject *)
   inv H1. inv H3.
   exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). 
-  assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)).
+  assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)).
     econstructor; eauto. rewrite Int.add_zero; auto. 
   exploit volatile_load_inject; eauto. intros [v' [A B]].
   exists f; exists v'; exists m1'; intuition. econstructor; eauto. 
@@ -934,8 +934,8 @@ Lemma volatile_store_inject:
   forall ge1 ge2 f chunk m1 b ofs v t m2 m1' b' ofs' v',
   symbols_inject f ge1 ge2 ->
   volatile_store ge1 chunk m1 b ofs v t m2 ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
-  val_inject f v v' ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f v v' ->
   Mem.inject f m1 m1' ->
   exists m2',
        volatile_store ge2 chunk m1' b' ofs' v' t m2'
@@ -950,7 +950,7 @@ Proof.
   inv AI. exploit Q; eauto. intros [A B]. subst delta. 
   rewrite Int.add_zero. exists m1'; split.
   constructor; auto. erewrite S; eauto. 
-  eapply eventval_match_inject; eauto. apply val_load_result_inject. auto.
+  eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto.
   intuition auto with mem.
 - (* normal store *)
   inversion AI; subst.
@@ -1058,7 +1058,7 @@ Proof.
 (* mem inject *)
   rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]].
   exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). 
-  assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto.
+  assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto.
   exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. 
   intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]].
   exists f'; exists vres'; exists m2'; intuition.
@@ -1552,10 +1552,10 @@ Lemma external_call_mem_inject:
   meminj_preserves_globals ge f ->
   external_call ef ge vargs m1 t vres m2 ->
   Mem.inject f m1 m1' ->
-  val_list_inject f vargs vargs' ->
+  Val.inject_list f vargs vargs' ->
   exists f', exists vres', exists m2',
      external_call ef ge vargs' m1' t vres' m2'
-    /\ val_inject f' vres vres'
+    /\ Val.inject f' vres vres'
     /\ Mem.inject f' m2 m2'
     /\ Mem.unchanged_on (loc_unmapped f) m1 m2
     /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
@@ -1644,11 +1644,11 @@ Proof.
 Qed.
 
 Lemma decode_longs_inject:
-  forall f tyl vl1 vl2, val_list_inject f vl1 vl2 -> val_list_inject f (decode_longs tyl vl1) (decode_longs tyl vl2).
+  forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list f (decode_longs tyl vl1) (decode_longs tyl vl2).
 Proof.
   induction tyl; simpl; intros. 
   auto.
-  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply val_longofwords_inject; auto. 
+  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. 
 Qed.
 
 Lemma encode_long_lessdef:
@@ -1659,10 +1659,10 @@ Proof.
 Qed.
 
 Lemma encode_long_inject:
-  forall f oty v1 v2, val_inject f v1 v2 -> val_list_inject f (encode_long oty v1) (encode_long oty v2).
+  forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list f (encode_long oty v1) (encode_long oty v2).
 Proof.
   intros. destruct oty as [[]|]; simpl; auto. 
-  constructor. apply val_hiword_inject; auto. constructor. apply val_loword_inject; auto. auto.
+  constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto.
 Qed.
 
 Lemma encode_long_has_type:
@@ -1736,10 +1736,10 @@ Lemma external_call_mem_inject':
   meminj_preserves_globals ge f ->
   external_call' ef ge vargs m1 t vres m2 ->
   Mem.inject f m1 m1' ->
-  val_list_inject f vargs vargs' ->
+  Val.inject_list f vargs vargs' ->
   exists f' vres' m2',
      external_call' ef ge vargs' m1' t vres' m2'
-  /\ val_list_inject f' vres vres'
+  /\ Val.inject_list f' vres vres'
   /\ Mem.inject f' m2 m2'
   /\ Mem.unchanged_on (loc_unmapped f) m1 m2
   /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
diff --git a/common/Memdata.v b/common/Memdata.v
index 96278a29..9c64563b 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -726,7 +726,7 @@ Inductive memval_inject (f: meminj): memval -> memval -> Prop :=
       forall n, memval_inject f (Byte n) (Byte n)
   | memval_inject_frag:
       forall v1 v2 q n,
-      val_inject f v1 v2 ->
+      Val.inject f v1 v2 ->
       memval_inject f (Fragment v1 q n) (Fragment v2 q n)
   | memval_inject_undef:
       forall mv, memval_inject f Undef mv.
@@ -738,7 +738,7 @@ Proof.
 Qed.
 
 (** [decode_val], applied to lists of memory values that are pairwise
-  related by [memval_inject], returns values that are related by [val_inject]. *)
+  related by [memval_inject], returns values that are related by [Val.inject]. *)
 
 Lemma proj_bytes_inject:
   forall f vl vl',
@@ -759,7 +759,7 @@ Lemma check_value_inject:
   list_forall2 (memval_inject f) vl vl' ->
   forall v v' q n,
   check_value n v q vl = true ->
-  val_inject f v v' -> v <> Vundef ->
+  Val.inject f v v' -> v <> Vundef ->
   check_value n v' q vl' = true.
 Proof.
   induction 1; intros; destruct n; simpl in *; auto. 
@@ -774,7 +774,7 @@ Qed.
 Lemma proj_value_inject:
   forall f q vl1 vl2,
   list_forall2 (memval_inject f) vl1 vl2 ->
-  val_inject f (proj_value q vl1) (proj_value q vl2).
+  Val.inject f (proj_value q vl1) (proj_value q vl2).
 Proof.
   intros. unfold proj_value. 
   inversion H; subst. auto. inversion H0; subst; auto.
@@ -819,26 +819,26 @@ Qed.
 Theorem decode_val_inject:
   forall f vl1 vl2 chunk,
   list_forall2 (memval_inject f) vl1 vl2 ->
-  val_inject f (decode_val chunk vl1) (decode_val chunk vl2).
+  Val.inject f (decode_val chunk vl1) (decode_val chunk vl2).
 Proof.
   intros. unfold decode_val. 
   destruct (proj_bytes vl1) as [bl1|] eqn:PB1.
   exploit proj_bytes_inject; eauto. intros PB2. rewrite PB2. 
   destruct chunk; constructor.
   assert (A: forall q fn,
-     val_inject f (Val.load_result chunk (proj_value q vl1))
+     Val.inject f (Val.load_result chunk (proj_value q vl1))
                   (match proj_bytes vl2 with
                    | Some bl => fn bl
                    | None => Val.load_result chunk (proj_value q vl2)
                    end)).
   { intros. destruct (proj_bytes vl2) as [bl2|] eqn:PB2.
     rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence.
-    apply val_load_result_inject. apply proj_value_inject; auto.
+    apply Val.load_result_inject. apply proj_value_inject; auto.
   }
   destruct chunk; auto.
 Qed.
 
-(** Symmetrically, [encode_val], applied to values related by [val_inject],
+(** Symmetrically, [encode_val], applied to values related by [Val.inject],
   returns lists of memory values that are pairwise
   related by [memval_inject]. *)
 
@@ -870,7 +870,7 @@ Proof.
 Qed.  
 
 Lemma inj_value_inject:
-  forall f v1 v2 q, val_inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2).
+  forall f v1 v2 q, Val.inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2).
 Proof.
   intros.
 Local Transparent inj_value.
@@ -880,7 +880,7 @@ Qed.
 
 Theorem encode_val_inject:
   forall f v1 v2 chunk,
-  val_inject f v1 v2 ->
+  Val.inject f v1 v2 ->
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
   intros. inversion H; subst; simpl; destruct chunk;
diff --git a/common/Memory.v b/common/Memory.v
index 45c2497b..3d781cac 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -2303,7 +2303,7 @@ Lemma load_inj:
   mem_inj f m1 m2 ->
   load chunk m1 b1 ofs = Some v1 ->
   f b1 = Some (b2, delta) ->
-  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2.
+  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros.
   exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents)#b2))).
@@ -2367,7 +2367,7 @@ Lemma store_mapped_inj:
   store chunk m1 b1 ofs v1 = Some n1 ->
   meminj_no_overlap f m1 ->
   f b1 = Some (b2, delta) ->
-  val_inject f v1 v2 ->
+  Val.inject f v1 v2 ->
   exists n2,
     store chunk m2 b2 (ofs + delta) v2 = Some n2
     /\ mem_inj f n1 n2.
@@ -3250,7 +3250,7 @@ Theorem valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
   valid_pointer m1 b (Int.unsigned ofs) = true ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   valid_pointer m2 b' (Int.unsigned ofs') = true.
 Proof.
   intros. inv H1.
@@ -3263,7 +3263,7 @@ Theorem weak_valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
   weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
 Proof.
   intros. inv H1.
@@ -3376,7 +3376,7 @@ Theorem load_inject:
   inject f m1 m2 ->
   load chunk m1 b1 ofs = Some v1 ->
   f b1 = Some (b2, delta) ->
-  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2.
+  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. inv H. eapply load_inj; eauto. 
 Qed.
@@ -3385,8 +3385,8 @@ Theorem loadv_inject:
   forall f m1 m2 chunk a1 a2 v1,
   inject f m1 m2 ->
   loadv chunk m1 a1 = Some v1 ->
-  val_inject f a1 a2 ->
-  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2.
+  Val.inject f a1 a2 ->
+  exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. inv H1; simpl in H0; try discriminate.
   exploit load_inject; eauto. intros [v2 [LOAD INJ]].
@@ -3414,7 +3414,7 @@ Theorem store_mapped_inject:
   inject f m1 m2 ->
   store chunk m1 b1 ofs v1 = Some n1 ->
   f b1 = Some (b2, delta) ->
-  val_inject f v1 v2 ->
+  Val.inject f v1 v2 ->
   exists n2,
     store chunk m2 b2 (ofs + delta) v2 = Some n2
     /\ inject f n1 n2.
@@ -3484,8 +3484,8 @@ Theorem storev_mapped_inject:
   forall f chunk m1 a1 v1 n1 m2 a2 v2,
   inject f m1 m2 ->
   storev chunk m1 a1 v1 = Some n1 ->
-  val_inject f a1 a2 ->
-  val_inject f v1 v2 ->
+  Val.inject f a1 a2 ->
+  Val.inject f v1 v2 ->
   exists n2,
     storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2.
 Proof.
@@ -3977,14 +3977,14 @@ Qed.
 
 Lemma val_lessdef_inject_compose:
   forall f v1 v2 v3,
-  Val.lessdef v1 v2 -> val_inject f v2 v3 -> val_inject f v1 v3.
+  Val.lessdef v1 v2 -> Val.inject f v2 v3 -> Val.inject f v1 v3.
 Proof.
   intros. inv H. auto. auto.
 Qed.
 
 Lemma val_inject_lessdef_compose:
   forall f v1 v2 v3,
-  val_inject f v1 v2 -> Val.lessdef v2 v3 -> val_inject f v1 v3.
+  Val.inject f v1 v2 -> Val.lessdef v2 v3 -> Val.inject f v1 v3.
 Proof.
   intros. inv H0. auto. inv H. auto.
 Qed.
@@ -4113,7 +4113,7 @@ Theorem store_inject_neutral:
   store chunk m b ofs v = Some m' ->
   inject_neutral thr m ->
   Plt b thr ->
-  val_inject (flat_inj thr) v v ->
+  Val.inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 Proof.
   intros; red.
diff --git a/common/Memtype.v b/common/Memtype.v
index d94c895f..43fc708f 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -927,7 +927,7 @@ Axiom weak_valid_pointer_extends:
 - if [f b = Some(b', ofs)], the block [b] of [m2] corresponds to
   a sub-block at offset [ofs] of the block [b'] in [m2].
 
-A memory injection [f] defines a relation [val_inject] between values
+A memory injection [f] defines a relation [Val.inject] between values
 that is the identity for integer and float values, and relocates pointer 
 values as prescribed by [f].  (See module [Values].)
 
@@ -1000,14 +1000,14 @@ Axiom valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
   valid_pointer m1 b (Int.unsigned ofs) = true ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   valid_pointer m2 b' (Int.unsigned ofs') = true.
 
 Axiom weak_valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
   weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
-  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
 
 Axiom inject_no_overlap:
@@ -1037,14 +1037,14 @@ Axiom load_inject:
   inject f m1 m2 ->
   load chunk m1 b1 ofs = Some v1 ->
   f b1 = Some (b2, delta) ->
-  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2.
+  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2.
 
 Axiom loadv_inject:
   forall f m1 m2 chunk a1 a2 v1,
   inject f m1 m2 ->
   loadv chunk m1 a1 = Some v1 ->
-  val_inject f a1 a2 ->
-  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2.
+  Val.inject f a1 a2 ->
+  exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2.
 
 Axiom loadbytes_inject:
   forall f m1 m2 b1 ofs len b2 delta bytes1,
@@ -1059,7 +1059,7 @@ Axiom store_mapped_inject:
   inject f m1 m2 ->
   store chunk m1 b1 ofs v1 = Some n1 ->
   f b1 = Some (b2, delta) ->
-  val_inject f v1 v2 ->
+  Val.inject f v1 v2 ->
   exists n2,
     store chunk m2 b2 (ofs + delta) v2 = Some n2
     /\ inject f n1 n2.
@@ -1085,8 +1085,8 @@ Axiom storev_mapped_inject:
   forall f chunk m1 a1 v1 n1 m2 a2 v2,
   inject f m1 m2 ->
   storev chunk m1 a1 v1 = Some n1 ->
-  val_inject f a1 a2 ->
-  val_inject f v1 v2 ->
+  Val.inject f a1 a2 ->
+  Val.inject f v1 v2 ->
   exists n2,
     storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2.
 
@@ -1221,7 +1221,7 @@ Axiom store_inject_neutral:
   store chunk m b ofs v = Some m' ->
   inject_neutral thr m ->
   Plt b thr ->
-  val_inject (flat_inj thr) v v ->
+  Val.inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 
 Axiom drop_inject_neutral:
diff --git a/common/Values.v b/common/Values.v
index 12b380b7..a4ead481 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1477,8 +1477,6 @@ Proof.
   intros. inv H; auto. 
 Qed.
 
-End Val.
-
 (** * Values and memory injections *)
 
 (** A memory injection [f] is a function from addresses to either [None]
@@ -1496,62 +1494,62 @@ Definition meminj : Type := block -> option (block * Z).
   as prescribed by the memory injection.  Moreover, [Vundef] values
   inject into any other value. *)
 
-Inductive val_inject (mi: meminj): val -> val -> Prop :=
-  | val_inject_int:
-      forall i, val_inject mi (Vint i) (Vint i)
-  | val_inject_long:
-      forall i, val_inject mi (Vlong i) (Vlong i)
-  | val_inject_float:
-      forall f, val_inject mi (Vfloat f) (Vfloat f)
-  | val_inject_single:
-      forall f, val_inject mi (Vsingle f) (Vsingle f)
-  | val_inject_ptr:
+Inductive inject (mi: meminj): val -> val -> Prop :=
+  | inject_int:
+      forall i, inject mi (Vint i) (Vint i)
+  | inject_long:
+      forall i, inject mi (Vlong i) (Vlong i)
+  | inject_float:
+      forall f, inject mi (Vfloat f) (Vfloat f)
+  | inject_single:
+      forall f, inject mi (Vsingle f) (Vsingle f)
+  | inject_ptr:
       forall b1 ofs1 b2 ofs2 delta,
       mi b1 = Some (b2, delta) ->
       ofs2 = Int.add ofs1 (Int.repr delta) ->
-      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
+      inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
   | val_inject_undef: forall v,
-      val_inject mi Vundef v.
+      inject mi Vundef v.
 
-Hint Constructors val_inject.
+Hint Constructors inject.
 
-Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= 
-  | val_nil_inject :
-      val_list_inject mi nil nil
-  | val_cons_inject : forall v v' vl vl' , 
-      val_inject mi v v' -> val_list_inject mi vl vl'->
-      val_list_inject mi (v :: vl) (v' :: vl').  
+Inductive inject_list (mi: meminj): list val -> list val-> Prop:= 
+  | inject_list_nil :
+      inject_list mi nil nil
+  | inject_list_cons : forall v v' vl vl' , 
+      inject mi v v' -> inject_list mi vl vl'->
+      inject_list mi (v :: vl) (v' :: vl').  
 
-Hint Resolve val_nil_inject val_cons_inject.
+Hint Resolve inject_list_nil inject_list_cons.
 
 Section VAL_INJ_OPS.
 
 Variable f: meminj.
 
-Lemma val_load_result_inject:
+Lemma load_result_inject:
   forall chunk v1 v2,
-  val_inject f v1 v2 ->
-  val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
+  inject f v1 v2 ->
+  inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
 Proof.
   intros. inv H; destruct chunk; simpl; econstructor; eauto.
 Qed.
 
-Remark val_add_inject:
+Remark add_inject:
   forall v1 v1' v2 v2',
-  val_inject f v1 v1' ->
-  val_inject f v2 v2' ->
-  val_inject f (Val.add v1 v2) (Val.add v1' v2').
+  inject f v1 v1' ->
+  inject f v2 v2' ->
+  inject f (Val.add v1 v2) (Val.add v1' v2').
 Proof.
   intros. inv H; inv H0; simpl; econstructor; eauto.
   repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
   repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
 Qed.
 
-Remark val_sub_inject:
+Remark sun_inject:
   forall v1 v1' v2 v2',
-  val_inject f v1 v1' ->
-  val_inject f v2 v2' ->
-  val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
+  inject f v1 v1' ->
+  inject f v2 v2' ->
+  inject f (Val.sub v1 v2) (Val.sub v1' v2').
 Proof.
   intros. inv H; inv H0; simpl; auto.
   econstructor; eauto. rewrite Int.sub_add_l. auto.
@@ -1559,10 +1557,10 @@ Proof.
   rewrite Int.sub_shifted. auto.
 Qed.
 
-Lemma val_cmp_bool_inject:
+Lemma cmp_bool_inject:
   forall c v1 v2 v1' v2' b,
-  val_inject f v1 v1' ->
-  val_inject f v2 v2' ->
+  inject f v1 v1' ->
+  inject f v2 v2' ->
   Val.cmp_bool c v1 v2 = Some b ->
   Val.cmp_bool c v1' v2' = Some b.
 Proof.
@@ -1602,10 +1600,10 @@ Hypothesis valid_different_ptrs_inj:
   b1' <> b2' \/
   Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 
-Lemma val_cmpu_bool_inject:
+Lemma cmpu_bool_inject:
   forall c v1 v2 v1' v2' b,
-  val_inject f v1 v1' ->
-  val_inject f v2 v2' ->
+  inject f v1 v1' ->
+  inject f v2 v2' ->
   Val.cmpu_bool valid_ptr1 c v1 v2 = Some b ->
   Val.cmpu_bool valid_ptr2 c v1' v2' = Some b.
 Proof.
@@ -1644,27 +1642,31 @@ Proof.
   now erewrite !valid_ptr_inj by eauto.
 Qed.
 
-Lemma val_longofwords_inject:
+Lemma longofwords_inject:
   forall v1 v2 v1' v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2').
+  inject f v1 v1' -> inject f v2 v2' -> inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2').
 Proof.
   intros. unfold Val.longofwords. inv H; auto. inv H0; auto.
 Qed.
 
-Lemma val_loword_inject:
-  forall v v', val_inject f v v' -> val_inject f (Val.loword v) (Val.loword v').
+Lemma loword_inject:
+  forall v v', inject f v v' -> inject f (Val.loword v) (Val.loword v').
 Proof.
   intros. unfold Val.loword; inv H; auto. 
 Qed.
 
-Lemma val_hiword_inject:
-  forall v v', val_inject f v v' -> val_inject f (Val.hiword v) (Val.hiword v').
+Lemma hiword_inject:
+  forall v v', inject f v v' -> inject f (Val.hiword v) (Val.hiword v').
 Proof.
   intros. unfold Val.hiword; inv H; auto. 
 Qed.
 
 End VAL_INJ_OPS.
 
+End Val.
+
+Notation meminj := Val.meminj.
+
 (** Monotone evolution of a memory injection. *)
 
 Definition inject_incr (f1 f2: meminj) : Prop :=
@@ -1684,33 +1686,33 @@ Qed.
 Lemma val_inject_incr:
   forall f1 f2 v v',
   inject_incr f1 f2 ->
-  val_inject f1 v v' ->
-  val_inject f2 v v'.
+  Val.inject f1 v v' ->
+  Val.inject f2 v v'.
 Proof.
   intros. inv H0; eauto.
 Qed.
 
-Lemma val_list_inject_incr:
+Lemma val_inject_list_incr:
   forall f1 f2 vl vl' ,
-  inject_incr f1 f2 -> val_list_inject f1 vl vl' ->
-  val_list_inject f2 vl vl'.
+  inject_incr f1 f2 -> Val.inject_list f1 vl vl' ->
+  Val.inject_list f2 vl vl'.
 Proof.
   induction vl; intros; inv H0. auto.
   constructor. eapply val_inject_incr; eauto. auto.
 Qed.
 
-Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
+Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr.
 
 Lemma val_inject_lessdef:
-  forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2.
+  forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.
 Proof.
   intros; split; intros.
   inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. 
   inv H; auto. inv H0. rewrite Int.add_zero; auto.
 Qed.
 
-Lemma val_list_inject_lessdef:
-  forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2.
+Lemma val_inject_list_lessdef:
+  forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> Val.inject_list (fun b => Some(b, 0)) vl1 vl2.
 Proof.
   intros; split.
   induction 1; constructor; auto. apply val_inject_lessdef; auto.
@@ -1723,7 +1725,7 @@ Definition inject_id : meminj := fun b => Some(b, 0).
 
 Lemma val_inject_id:
   forall v1 v2,
-  val_inject inject_id v1 v2 <-> Val.lessdef v1 v2.
+  Val.inject inject_id v1 v2 <-> Val.lessdef v1 v2.
 Proof.
   intros; split; intros.
   inv H; auto. 
@@ -1747,8 +1749,8 @@ Definition compose_meminj (f f': meminj) : meminj :=
 
 Lemma val_inject_compose:
   forall f f' v1 v2 v3,
-  val_inject f v1 v2 -> val_inject f' v2 v3 ->
-  val_inject (compose_meminj f f') v1 v3.
+  Val.inject f v1 v2 -> Val.inject f' v2 v3 ->
+  Val.inject (compose_meminj f f') v1 v3.
 Proof.
   intros. inv H; auto; inv H0; auto. econstructor.
   unfold compose_meminj; rewrite H1; rewrite H3; eauto. 
diff --git a/ia32/Op.v b/ia32/Op.v
index ecc67c46..33f30aa5 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -755,30 +755,30 @@ Hypothesis valid_different_pointers_inj:
 
 Ltac InvInject :=
   match goal with
-  | [ H: val_inject _ (Vint _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vint _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vfloat _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vptr _ _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ nil _ |- _ ] =>
+  | [ H: Val.inject_list _ nil _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ (_ :: _) _ |- _ ] =>
+  | [ H: Val.inject_list _ (_ :: _) _ |- _ ] =>
       inv H; InvInject
   | _ => idtac
   end.
 
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; simpl in H0; inv H0; auto.
-  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
@@ -789,7 +789,7 @@ Qed.
 
 Ltac TrivialExists :=
   match goal with
-  | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
+  | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
       exists v1; split; auto
   | _ => idtac
   end.
@@ -798,32 +798,32 @@ Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_addressing addr) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing ge1 sp1 addr vl1 = Some v1 ->
-  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. inv H5; simpl; auto.
-  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; simpl; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto. inv H5; simpl; auto.
+  apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. inv H3; simpl; auto.
   apply H; simpl; auto.
-  apply Values.val_add_inject; auto. apply H; simpl; auto.
-  apply Values.val_add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto.
-  apply Values.val_add_inject; auto.
+  apply Values.Val.add_inject; auto. apply H; simpl; auto.
+  apply Values.Val.add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto.
+  apply Values.Val.add_inject; auto.
 Qed.
 
 Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_operation op) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
-  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
@@ -959,7 +959,7 @@ Proof.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
-  rewrite <- val_list_inject_lessdef. eauto. auto.
+  rewrite <- val_inject_list_lessdef. eauto. auto.
 Qed.
 
 Lemma eval_operation_lessdef:
@@ -969,10 +969,10 @@ Lemma eval_operation_lessdef:
   eval_operation genv sp op vl1 m1 = Some v1 ->
   exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_operation genv sp op vl2 m2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   apply valid_pointer_extends; auto.
   apply weak_valid_pointer_extends; auto.
@@ -991,10 +991,10 @@ Lemma eval_addressing_lessdef:
   eval_addressing genv sp addr vl1 = Some v1 ->
   exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_addressing genv sp addr vl2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_addressing_inj with (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
@@ -1018,7 +1018,7 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
+  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
@@ -1027,7 +1027,7 @@ Qed.
 
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
@@ -1041,11 +1041,11 @@ Qed.
 
 Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
   exists v2, 
      eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_addressing. simpl.
@@ -1055,12 +1055,12 @@ Qed.
 
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
   exists v2,
      eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_operation. simpl.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 4c1168cd..3ff08791 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -677,32 +677,32 @@ Hypothesis valid_different_pointers_inj:
 
 Ltac InvInject :=
   match goal with
-  | [ H: val_inject _ (Vint _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vint _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vfloat _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vsingle _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vsingle _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
+  | [ H: Val.inject _ (Vptr _ _) _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ nil _ |- _ ] =>
+  | [ H: Val.inject_list _ nil _ |- _ ] =>
       inv H; InvInject
-  | [ H: val_list_inject _ (_ :: _) _ |- _ ] =>
+  | [ H: Val.inject_list _ (_ :: _) _ |- _ ] =>
       inv H; InvInject
   | _ => idtac
   end.
 
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; simpl in H0; inv H0; auto.
-  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; try discriminate; auto.
@@ -711,7 +711,7 @@ Qed.
 
 Ltac TrivialExists :=
   match goal with
-  | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
+  | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
       exists v1; split; auto
   | _ => idtac
   end.
@@ -720,20 +720,20 @@ Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_operation op) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
-  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
-  apply Values.val_add_inject; auto. 
+  apply Values.Val.add_inject; auto. 
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. apply GL; simpl; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto.
+  apply Values.Val.add_inject; auto. apply GL; simpl; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
     destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. 
@@ -797,16 +797,16 @@ Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
       In id (globals_addressing addr) ->
-      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
-  val_inject f sp1 sp2 ->
-  val_list_inject f vl1 vl2 ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing ge1 sp1 addr vl1 = Some v1 ->
-  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
+  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists;
-    auto using Values.val_add_inject.
+    auto using Values.Val.add_inject.
   apply H; simpl; auto.
-  apply Values.val_add_inject; auto. apply H; simpl; auto.
+  apply Values.Val.add_inject; auto. apply H; simpl; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -872,7 +872,7 @@ Proof.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends; auto.
   apply valid_different_pointers_extends; auto.
-  rewrite <- val_list_inject_lessdef. eauto. auto.
+  rewrite <- val_inject_list_lessdef. eauto. auto.
 Qed.
 
 Lemma eval_operation_lessdef:
@@ -882,10 +882,10 @@ Lemma eval_operation_lessdef:
   eval_operation genv sp op vl1 m1 = Some v1 ->
   exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_operation genv sp op vl2 m2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   apply valid_pointer_extends; auto.
   apply weak_valid_pointer_extends; auto.
@@ -903,10 +903,10 @@ Lemma eval_addressing_lessdef:
   eval_addressing genv sp addr vl1 = Some v1 ->
   exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.
 Proof.
-  intros. rewrite val_list_inject_lessdef in H.
+  intros. rewrite val_inject_list_lessdef in H.
   assert (exists v2 : val,
           eval_addressing genv sp addr vl2 = Some v2
-          /\ val_inject (fun b => Some(b, 0)) v1 v2).
+          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_addressing_inj with (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
@@ -930,7 +930,7 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
+  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
@@ -939,7 +939,7 @@ Qed.
 
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
@@ -953,11 +953,11 @@ Qed.
 
 Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
   exists v2, 
      eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_addressing. simpl.
@@ -967,12 +967,12 @@ Qed.
 
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
-  val_list_inject f vl1 vl2 ->
+  Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
   eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
   exists v2,
      eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
-  /\ val_inject f v1 v2.
+  /\ Val.inject f v1 v2.
 Proof.
   intros. 
   rewrite eval_shift_stack_operation. simpl.