diff options
| author | Brian Campbell | 2018-05-28 16:25:00 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-28 16:25:00 +0100 |
| commit | 02244be10529f3fa103890e920c7c34fca5f181e (patch) | |
| tree | 2c1802b091a2c59a0b858742cb81fd06eb8d44bd /test | |
| parent | 302048dfccaef8614af504875a526b43d4e4ab93 (diff) | |
Coq: add option to produce axioms for unimplemented functions
Useful for partial test cases (e.g., some of the typechecking tests)
Also a bonus warning for such functions in normal use
Diffstat (limited to 'test')
| -rwxr-xr-x | test/coq/run_tests.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index a9c6ab24..f782ed80 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -51,7 +51,7 @@ cd $DIR for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`; do - if $SAILDIR/sail -coq -o out $TESTSDIR/$i &>/dev/null; + if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null; then if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null; then |