From b0c78262e4c8a8670c6a111cb3bcac00dc445251 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 26 Jul 2018 14:11:42 +0100
Subject: Coq: patterns on bit literals

---
 src/rewrites.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2729e7cd..5a903a40 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4036,6 +4036,8 @@ struct
 
 type rlit =
   | RL_unit
+  (* TODO: zero and one are currently replaced by RL_inf to deal with BU;
+     needs more careful thought about semantics of BU *)
   | RL_zero
   | RL_one
   | RL_true
@@ -4053,8 +4055,8 @@ let string_of_rlit = function
 let rlit_of_lit (L_aux (l,_)) =
   match l with
   | L_unit -> RL_unit
-  | L_zero -> RL_zero
-  | L_one -> RL_one
+  | L_zero -> (*RL_zero*) RL_inf
+  | L_one -> (*RL_one*) RL_inf
   | L_true -> RL_true
   | L_false -> RL_false
   | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> RL_inf
@@ -4063,8 +4065,8 @@ let rlit_of_lit (L_aux (l,_)) =
 let inv_rlit_of_lit (L_aux (l,_)) =
   match l with
   | L_unit -> []
-  | L_zero -> [RL_one]
-  | L_one -> [RL_zero]
+  | L_zero -> (*[RL_one]*) [RL_inf]
+  | L_one -> (*[RL_zero]*) [RL_inf]
   | L_true -> [RL_false]
   | L_false -> [RL_true]
   | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> [RL_inf]
-- 
cgit v1.2.3