Coq: firstorder is better at the boolean goals

1 files changed, 3 insertions, 2 deletions

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
  ].