aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-02-19 11:51:04 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-02-19 11:53:40 +0100
commit9aa2d99fb1ad6b348142fce244f277b9dd25017f (patch)
tree22dc54480f0b3c94cf214e05e1d3972253fbb668 /theories/Lists
parent37479c1b59b7492abb5c89a42c5a76d4cd9d48cd (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 'theories/Lists')
0 files changed, 0 insertions, 0 deletions