diff options
author | 2016-02-19 11:51:04 +0100 | |
---|---|---|
committer | 2016-02-19 11:53:40 +0100 | |
commit | 9aa2d99fb1ad6b348142fce244f277b9dd25017f (patch) | |
tree | 22dc54480f0b3c94cf214e05e1d3972253fbb668 /test-suite | |
parent | 37479c1b59b7492abb5c89a42c5a76d4cd9d48cd (diff) |
STM: Print/Extraction have to be skipped if -quick
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/vio/print.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/vio/print.v b/test-suite/vio/print.v new file mode 100644 index 000000000..9c36a463c --- /dev/null +++ b/test-suite/vio/print.v @@ -0,0 +1,10 @@ +Lemma a : True. +Proof. +idtac. +exact I. +Qed. + +Print a. + +Lemma b : False. +Admitted. |