From 576fb915bc281ea8e59eba896e3404d2f85e918c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Mar 2019 10:41:33 +0000
Subject: Coq: add a little bit of boolean solving Just enough for RISC-V to go
 through

---
 lib/coq/Sail2_values.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 1b5da853..e6c5e786 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1208,6 +1208,14 @@ prepare_for_solver;
  | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
+   (* Booleans - and_boolMP *)
+ | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => 
+     constructor; intros l r H1 H2;
+     solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
+   end
+ | match goal with |- context [@eq _ _ _] =>
+     constructor; intuition
+   end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get
-- 
cgit v1.2.3