Coq test running update

- ex_cons_infer uses an existential type in a way that's not supported yet
- Replicate needs --strict-bitvectors

test/coq/run_tests.sh

@@ -47,7 +47,7 @@ function check_tests_dir {
     TESTSDIR="$1"
     for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`;
     do
-        if $SAIL -coq -coq-lib-style stdpp -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
+        if $SAIL -coq -coq-lib-style stdpp -dcoq_undef_axioms --strict-bitvector -o out $TESTSDIR/$i &>/dev/null;
         then
     	if coqc $COQOPTS out_types.v &>/dev/null &&
     	   coqc $COQOPTS out.v &>/dev/null;

test/coq/skip

@@ -51,6 +51,7 @@ XXXXX Need to be built against stdpp version of Sail (for now)
 concurrency_interface_dec.sail
 concurrency_interface_inc.sail
 XXXXX Would need to turn a term with existential type into a dependent pair
+ex_cons_infer.sail
 ex_list_infer.sail
 ex_vector_infer.sail
 XXXXX Would need float types in coq-sail