2 files changed, 0 insertions, 49 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 741fa921..bae8381e 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -89,20 +89,6 @@ Defined.
 Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E :=
   x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)).
 
-Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E.
-refine (
- l >>= (fun l => if l then r >>= fun r => if r then returnm (left _) else returnm (right _) else returnm (right _))
-).
-all: tauto.
-Defined.
-
-Definition or_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P \/ Q)) E.
-refine (
- l >>= (fun l => if l then returnm (left _) else r >>= fun r => if r then returnm (left _) else returnm (right _))
-).
-all: tauto.
-Defined.
-
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
 match b with
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index bd2c0fdb..1b5da853 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -45,35 +45,6 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
-(* The informative boolean type. *)
-
-Definition Bool (P : Prop) : Type := {P} + {~P}.
-
-Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P.
-refine (if sumbool_of_bool b then left _ else right _);
-destruct H; subst;
-intuition.
-Defined.
-
-Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false.
-
-Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P.
-destruct b; simpl; intuition.
-Qed.
-Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P.
-destruct b; simpl; intuition.
-Qed.
-
-Definition and_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P /\ Q).
-refine (if l then if r then left _ else right _ else right _).
-all: tauto.
-Defined.
-
-Definition or_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P \/ Q).
-refine (if l then left _ else if r then left _ else right _).
-all: tauto.
-Defined.
-
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
@@ -1123,11 +1094,6 @@ Ltac extract_properties :=
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
     change (projT1 (existT _ x Hx)) with x in * end.
-(* We could also destruct any remaining Bools, if necessary. *)
-Ltac extract_Bool_props :=
-  repeat match goal with
-  | H:projBool _ = true |- _ => rewrite projBool_true in H
-  | H:projBool _ = false |- _ => rewrite projBool_false in H end.
 (* TODO: hyps, too? *)
 Ltac reduce_list_lengths :=
   repeat match goal with |- context [length_list ?X] => 
@@ -1193,7 +1159,6 @@ Ltac prepare_for_solver :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
- extract_Bool_props;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  destruct_exists;