4 files changed, 16 insertions, 16 deletions
diff --git a/mips/hgen/herdtools_types_to_shallow_types.hgen b/mips/hgen/herdtools_types_to_shallow_types.hgen
index 115de27c..5a0e3bfc 100644
--- a/mips/hgen/herdtools_types_to_shallow_types.hgen
+++ b/mips/hgen/herdtools_types_to_shallow_types.hgen
@@ -100,21 +100,21 @@ let translate_imm16 name value =
 let translate_imm5 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
 let translate_bool name = function
-  | true -> Sail_values.I
-  | false -> Sail_values.O
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
 
 let translate_wordsize _ = function
- | MIPSByte -> Mips_embed_types.B0
+ | MIPSByte -> Mips_embed_types.B2
  | MIPSHalf -> Mips_embed_types.H
  | MIPSWord -> Mips_embed_types.W
  | MIPSDouble -> Mips_embed_types.D
 
 let translate_cmp _ = function
-  | MIPS_EQ  -> EQ_
+  | MIPS_EQ  -> EQ'
   | MIPS_NE  -> NE
   | MIPS_GE  -> GE
   | MIPS_GEU -> GEU
-  | MIPS_GT  -> GT_
+  | MIPS_GT  -> GT'
   | MIPS_LE  -> LE
-  | MIPS_LT  -> LT_
+  | MIPS_LT  -> LT'
   | MIPS_LTU -> LTU
diff --git a/mips/hgen/shallow_types_to_herdtools_types.hgen b/mips/hgen/shallow_types_to_herdtools_types.hgen
index 88743ac0..a02d83b7 100644
--- a/mips/hgen/shallow_types_to_herdtools_types.hgen
+++ b/mips/hgen/shallow_types_to_herdtools_types.hgen
@@ -17,23 +17,23 @@ let translate_out_simm16 imm = translate_out_signed_int imm 16
 let translate_out_imm5 imm = translate_out_int imm
 
 let translate_out_bool = function
-  | Sail_values.I  -> true
-  | Sail_values.O -> false
+  | Sail_values.B1  -> true
+  | Sail_values.B0 -> false
   | _ -> failwith "translate_out_bool Undef"
 
 
 let translate_out_wordWidth = function
-    | Mips_embed_types.B0 -> MIPSByte
+    | Mips_embed_types.B2 -> MIPSByte
     | Mips_embed_types.H -> MIPSHalf
     | Mips_embed_types.W -> MIPSWord
     | Mips_embed_types.D -> MIPSDouble
 
 let translate_out_cmp = function
-    | Mips_embed_types.EQ_ -> MIPS_EQ  (* equal *)
+    | Mips_embed_types.EQ' -> MIPS_EQ  (* equal *)
     | Mips_embed_types.NE -> MIPS_NE  (* not equal *)
     | Mips_embed_types.GE -> MIPS_GE  (* signed greater than or equal *)
     | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) 
-    | Mips_embed_types.GT_ -> MIPS_GT  (* signed strictly greater than *) 
+    | Mips_embed_types.GT' -> MIPS_GT  (* signed strictly greater than *) 
     | Mips_embed_types.LE -> MIPS_LE  (* signed less than or equal *) 
-    | Mips_embed_types.LT_ -> MIPS_LT  (* signed strictly less than *) 
+    | Mips_embed_types.LT' -> MIPS_LT  (* signed strictly less than *) 
     | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) 
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem
index d59213b8..41a6726f 100644
--- a/mips/mips_extras_embed.lem
+++ b/mips/mips_extras_embed.lem
@@ -33,9 +33,9 @@ val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
 
 let MEMval (_,_,v)                 = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 let MEMval_tag (_,_,v)             = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 
 
 val MEM_sync  : unit -> M unit
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem
index 6070df09..502fe102 100644
--- a/mips/mips_extras_embed_sequential.lem
+++ b/mips/mips_extras_embed_sequential.lem
@@ -33,9 +33,9 @@ val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
 
 let MEMval (_,_,v)                 = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 let MEMval_tag (_,_,v)             = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 
 
 val MEM_sync  : unit -> M unit