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

1 files changed, 26 insertions, 26 deletions

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.