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

6 files changed, 63 insertions, 63 deletions

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.