update kvx

1 files changed, 25 insertions, 25 deletions

diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
index 74b9b62b..c6ad70ab 100644
--- a/kvx/Asmblockgenproof1.v
+++ b/kvx/Asmblockgenproof1.v
@@ -256,7 +256,7 @@ Lemma transl_compu_correct:
   exists rs',
      exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ (Val_cmpu_bool cmp rs#r1 rs#r2 = Some b ->
+  /\ (Val.mxcmpu_bool cmp rs#r1 rs#r2 = Some b ->
        exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -272,8 +272,8 @@ Proof.
       assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val_cmpu_bool cmp rs#r1 rs#r2) as cmpubool.
-      destruct cmp; simpl; unfold Val_cmpu;
+      remember (Val.mxcmpu_bool cmp rs#r1 rs#r2) as cmpubool.
+      destruct cmp; simpl; unfold Val.mxcmpu;
         rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
       destruct b0; simpl; auto.
     }
@@ -285,7 +285,7 @@ Lemma transl_compui_correct:
   exists rs',
      exec_straight ge (transl_compi cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ (Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
+  /\ (Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b ->
        exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -301,8 +301,8 @@ Proof.
       assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val_cmpu_bool cmp rs#r1 (Vint n)) as cmpubool.
-      destruct cmp; simpl; unfold Val_cmpu;
+      remember (Val.mxcmpu_bool cmp rs#r1 (Vint n)) as cmpubool.
+      destruct cmp; simpl; unfold Val.mxcmpu;
         rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
       destruct b0; simpl; auto.
     }
@@ -656,7 +656,7 @@ Lemma transl_complu_correct:
   exists rs',
      exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ ( Val_cmplu_bool cmp rs#r1 rs#r2 = Some b ->
+  /\ ( Val.mxcmplu_bool cmp rs#r1 rs#r2 = Some b ->
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -672,9 +672,9 @@ Proof.
       assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val_cmplu_bool cmp rs#r1 rs#r2) as cmpbool.
+      remember (Val.mxcmplu_bool cmp rs#r1 rs#r2) as cmpbool.
       destruct cmp; simpl;
-      unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
       destruct b0; simpl; auto.
     }
     rewrite H0. simpl; auto.
@@ -685,7 +685,7 @@ Lemma transl_compilu_correct:
   exists rs',
      exec_straight ge (transl_compil cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
+  /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b ->
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -701,9 +701,9 @@ Proof.
       assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val_cmplu_bool cmp rs#r1 (Vlong n)) as cmpbool.
+      remember (Val.mxcmplu_bool cmp rs#r1 (Vlong n)) as cmpbool.
       destruct cmp; simpl;
-      unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
       destruct b0; simpl; auto.
     }
     rewrite H0. simpl; auto.
@@ -715,7 +715,7 @@ Lemma transl_opt_compuimm_correct:
   exists rs', exists insn,
      exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
+  /\ ( Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b ->
        exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
 Proof.
@@ -791,7 +791,7 @@ Lemma transl_opt_compluimm_correct:
   exists rs', exists insn,
      exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
-  /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
+  /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b ->
        exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
 Proof.
@@ -859,7 +859,7 @@ Proof.
     destruct cmp; discriminate.
 Qed.
 
-Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core.
+Local Hint Resolve Val.mxcmpu_bool_correct Val.mxcmplu_bool_correct: core.
 
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m' tbb,
@@ -988,7 +988,7 @@ Proof.
     split.
     * constructor. eexact A'.
     * split; auto.
-      { apply C'; auto. eapply Val_cmplu_bool_correct; eauto. }
+      { apply C'; auto. eapply Val.mxcmplu_bool_correct; eauto. }
 
 (* Ccompf *)
 - exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
@@ -1078,7 +1078,7 @@ Lemma transl_cond_int32u_correct:
   forall cmp rd r1 r2 k rs m,
   exists rs',
      exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
-  /\ rs'#rd = Val_cmpu cmp rs#r1 rs#r2
+  /\ rs'#rd = Val.mxcmpu cmp rs#r1 rs#r2
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
   intros. destruct cmp; simpl. 
@@ -1122,7 +1122,7 @@ Lemma transl_cond_int64u_correct:
   forall cmp rd r1 r2 k rs m,
   exists rs',
      exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
-  /\ rs'#rd = Val_cmplu cmp rs#r1 rs#r2
+  /\ rs'#rd = Val.mxcmplu cmp rs#r1 rs#r2
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
   intros. destruct cmp; simpl. 
@@ -1163,7 +1163,7 @@ Proof.
   split; intros; Simpl.
 Qed.
 
-Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core.
+Local Hint Resolve Val.mxcmpu_correct Val.mxcmplu_correct: core.
 
 Lemma transl_condimm_int32u_correct:
   forall cmp rd r1 n k rs m,
@@ -1279,12 +1279,12 @@ Proof.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
   unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
-  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap.
+  replace (Cge) with (swap_comparison Cle); auto. rewrite Float32.cmp_swap.
   destruct (Float32.cmp _ _ _); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
   unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
-  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
+  replace (Clt) with (swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
   destruct (Float32.cmp _ _ _); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
@@ -1345,12 +1345,12 @@ Proof.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
   unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
-  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap.
+  replace (Cge) with (swap_comparison Cle); auto. rewrite Float.cmp_swap.
   destruct (Float.cmp _ _ _); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
   unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
-  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap.
+  replace (Clt) with (swap_comparison Cgt); auto. rewrite Float.cmp_swap.
   destruct (Float.cmp _ _ _); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
@@ -1374,7 +1374,7 @@ Proof.
   exploit transl_cond_int32s_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; eauto.
 + (* cmpu *)
   exploit transl_cond_int32u_correct; eauto. simpl. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B; eapply Val_cmpu_correct.
+  exists rs'; repeat split; eauto. rewrite B; eapply Val.mxcmpu_correct.
 + (* cmpimm *)
   apply transl_condimm_int32s_correct; eauto with asmgen.
 + (* cmpuimm *)
@@ -1385,7 +1385,7 @@ Proof.
 + (* cmplu *)
   exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C).
   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
-  eapply Val_cmplu_correct.
+  eapply Val.mxcmplu_correct.
 + (* cmplimm *)
   exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. 
   intros (rs' & A & B & C).