From 056658bd2986d9e12ac07a54d25c08eb8a62ff60 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@lilo.org>
Date: Wed, 28 Jul 2021 10:32:09 +0200
Subject: remove todos, clean

---
 common/Values.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'common')

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.
-- 
cgit