From 94e2f401263c7efc69f7d2b731827dc41bd8c1b8 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 2 Aug 2019 11:39:25 +0100
Subject: Fix up some edge cases with the bitvector/polyvector split Mostly in
 the Coq backend, plus a few testcases that use bitvector builtins on
 poly-vectors (which works on some backends, but not Coq). Also handle some
 additional list inclusion proofs in Coq.

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index fc97fcc6..15bdaea4 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1704,10 +1704,10 @@ Ltac main_solver :=
  | match goal with |- context [Z.mul] => nia end
  (* If we have a disjunction from a set constraint on a variable we can often
     solve a goal by trying them (admittedly this is quite heavy handed...) *)
- | subst;
+ | subst; drop_Z_exists;
    let aux x :=
     is_var x;
-    intuition (subst;auto)
+    intuition (subst;auto with datatypes)
    in
    match goal with
    | _:(@eq Z _ ?x) \/ (@eq Z _ ?x) \/ _ |- context[?x] => aux x
-- 
cgit v1.2.3