diff options
4 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out new file mode 100644 index 0000000000..68dbaeb7b3 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.out @@ -0,0 +1,4 @@ +While loading initial state: +Warning: There is no flag or option with this name: "Extraction Optimize". +[unknown-option,option] +Extraction Optimize is on diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v new file mode 100644 index 0000000000..9a70674b02 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *) + +Test Extraction Optimize. diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out new file mode 100644 index 0000000000..76bb2016eb --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.out @@ -0,0 +1 @@ +Extraction Optimize is off diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v new file mode 100644 index 0000000000..7622d6ff52 --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *) + +Test Extraction Optimize. |