[MERGE] BTL into kvx-work (replacing RTLpath)

2 files changed, 17 insertions, 5 deletions

diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 275e6a71..83a485b0 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -1,6 +1,7 @@
 open Maps
 open Camlcoq
 open Registers
+open RTLcommonaux
 
 let debug_flag = ref false
 
@@ -128,11 +129,8 @@ end
 
 
 let print_instructions insts code =
-  let get_some = function
-  | None -> failwith "Did not get some"
-  | Some thing -> thing
-  in if (!debug_flag) then begin
-    debug "[\n";
+  if (!debug_flag) then begin
+    debug "[ ";
     List.iter (
       fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code))
     ) insts; debug "  ]"
diff --git a/common/Values.v b/common/Values.v
index 9353366d..87ebea00 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2016,6 +2016,20 @@ Proof.
   destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
+Theorem swap_cmpf_bool:
+  forall c x y,
+  Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
+Qed.
+
+Theorem swap_cmpfs_bool:
+  forall c x y,
+  Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
+Qed.
+
 Theorem cmp_ne_0_optbool:
   forall ob, cmp Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
 Proof.