From 98f447e1ca70999350dac4b7a0d3fbce5c64071b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 5 Mar 2019 15:13:15 +0000
Subject: Coq: firstorder is better at the boolean goals

---
 lib/coq/Sail2_values.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index ba94a237..fa40e01a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1213,8 +1213,9 @@ prepare_for_solver;
      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
+ | match goal with |- context [@eq bool _ _] =>
+     (* Don't use auto for the fallback to keep runtime down *)
+     firstorder fail
    end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
-- 
cgit v1.2.3