From 9aa2d99fb1ad6b348142fce244f277b9dd25017f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Feb 2016 11:51:04 +0100 Subject: 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. --- test-suite/vio/print.v | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test-suite/vio/print.v (limited to 'test-suite') 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. -- cgit v1.2.3