Val_cmp* -> Val.mxcmp*

1 files changed, 17 insertions, 17 deletions

diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index 754b49d6..61d77881 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -896,8 +896,8 @@ Ltac TranslOpBase :=
 Lemma compare_int_spec: forall rs v1 v2,
   let rs' := compare_int rs v1 v2 in
      rs'#CN = (Val.negative (Val.sub v1 v2))
-  /\ rs'#CZ = (Val_cmpu Ceq v1 v2)
-  /\ rs'#CC = (Val_cmpu Cge v1 v2)
+  /\ rs'#CZ = (Val.mxcmpu Ceq v1 v2)
+  /\ rs'#CC = (Val.mxcmpu Cge v1 v2)
   /\ rs'#CV = (Val.sub_overflow v1 v2).
 Proof.
   intros; unfold rs'; auto.
@@ -912,7 +912,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmpu; simpl. destruct c; simpl.
+  unfold Val.mxcmpu; simpl. destruct c; simpl.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.eq i i0); auto.
   - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
@@ -924,7 +924,7 @@ Proof.
 Qed.
 
 Lemma eval_testcond_compare_uint: forall c v1 v2 b rs,
-  Val_cmpu_bool c v1 v2 = Some b ->
+  Val.mxcmpu_bool c v1 v2 = Some b ->
   eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b.
 Proof.
   intros. generalize (compare_int_spec rs v1 v2). 
@@ -932,7 +932,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmpu; simpl. destruct c; simpl.
+  unfold Val.mxcmpu; simpl. destruct c; simpl.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.ltu i i0); auto.
@@ -944,8 +944,8 @@ Qed.
 Lemma compare_long_spec: forall rs v1 v2,
   let rs' := compare_long rs v1 v2 in
      rs'#CN = (Val.negativel (Val.subl v1 v2))
-  /\ rs'#CZ = (Val_cmplu Ceq v1 v2)
-  /\ rs'#CC = (Val_cmplu Cge v1 v2)
+  /\ rs'#CZ = (Val.mxcmplu Ceq v1 v2)
+  /\ rs'#CC = (Val.mxcmplu Cge v1 v2)
   /\ rs'#CV = (Val.subl_overflow v1 v2).
 Proof.
   intros; unfold rs'; auto.
@@ -977,7 +977,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmplu; simpl. destruct c; simpl.
+  unfold Val.mxcmplu; simpl. destruct c; simpl.
   - destruct (Int64.eq i i0); auto.
   - destruct (Int64.eq i i0); auto.
   - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
@@ -989,12 +989,12 @@ Proof.
 Qed.
 
 Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs,
-  Val_cmplu_bool c v1 v2 = Some b ->
+  Val.mxcmplu_bool c v1 v2 = Some b ->
   eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b.
 Proof.
   intros. generalize (compare_long_spec rs v1 v2). 
   set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
-  unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu.
+  unfold eval_testcond; rewrite B, C, D, E; unfold Val.mxcmplu.
   destruct v1; try discriminate; destruct v2; try discriminate; simpl in H.
   - (* int-int *)
     inv H. destruct c; simpl.
@@ -1207,7 +1207,7 @@ Proof.
   - (* Ccomplu *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
     split; intros. apply eval_testcond_compare_ulong; auto.
-    erewrite Val_cmplu_bool_correct; eauto.
+    erewrite Val.mxcmplu_bool_correct; eauto.
     destruct r; reflexivity || discriminate.
   - (* Ccomplimm *)
     destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
@@ -1228,19 +1228,19 @@ Proof.
     destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
     + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
       split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto.
+      erewrite Val.mxcmplu_bool_correct; eauto.
       destruct r; reflexivity || discriminate.
     + econstructor; split.
       apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
       split; intros. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto.
+      erewrite Val.mxcmplu_bool_correct; eauto.
       destruct r; reflexivity || discriminate.
     + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
       econstructor; split.
       eapply exec_straight_trans. eexact A. apply exec_straight_one.
       simpl. rewrite B, C by eauto with asmgen. eauto.
       split; intros. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto. 
+      erewrite Val.mxcmplu_bool_correct; eauto. 
       transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
   - (* Ccomplshift *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
@@ -1249,7 +1249,7 @@ Proof.
   - (* Ccomplushift *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
     split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
-    erewrite Val_cmplu_bool_correct; eauto. 
+    erewrite Val.mxcmplu_bool_correct; eauto. 
     destruct r; reflexivity || discriminate.
   - (* Cmasklzero *)
     destruct (is_logical_imm64 n).
@@ -1368,7 +1368,7 @@ Local Opaque transl_cond transl_cond_branch_default.
     apply Int.same_if_eq in N0; subst n; ArgsInv.
     + (* Ccompuimm Cne 0 *)
       econstructor; split. econstructor.
-      split; auto. simpl. apply Val_cmpu_bool_correct in EV.
+      split; auto. simpl. apply Val.mxcmpu_bool_correct in EV.
       unfold incrPC. Simpl. rewrite EV. auto.
     + (* Ccompuimm Ceq 0 *)
       monadInv TR. ArgsInv. simpl in *.
@@ -1408,7 +1408,7 @@ Local Opaque transl_cond transl_cond_branch_default.
     apply Int64.same_if_eq in N0; subst n; ArgsInv.
     + (* Ccompluimm Cne 0 *)
       econstructor; split. econstructor.
-      split; auto. simpl. apply Val_cmplu_bool_correct in EV.
+      split; auto. simpl. apply Val.mxcmplu_bool_correct in EV.
       unfold incrPC. Simpl. rewrite EV. auto.
     + (* Ccompluimm Ceq 0 *)
       econstructor; split. econstructor.