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

1 files changed, 35 insertions, 35 deletions

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.