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.

1 files changed, 2 insertions, 2 deletions

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