diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 5 |
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 ]. |