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

5 files changed, 113 insertions, 111 deletions

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.