From e9fa9cbdc761f8c033e9b702f7485982faed3f7d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 30 Apr 2015 19:26:11 +0200
Subject: Long-overdue renaming: val_inject -> Val.inject, etc, for consistency
 with Val.lessdef, etc.

---
 cfrontend/Cminorgenproof.v    | 60 +++++++++++++++++++++----------------------
 cfrontend/Cop.v               | 52 ++++++++++++++++++-------------------
 cfrontend/Initializersproof.v | 12 ++++-----
 cfrontend/SimplLocalsproof.v  | 36 +++++++++++++-------------
 4 files changed, 80 insertions(+), 80 deletions(-)

(limited to 'cfrontend')

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.
-- 
cgit