coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-02-19	STM: Print/Extraction have to be skipped if -quick	Enrico Tassi
	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.