aboutsummaryrefslogtreecommitdiff
path: root/test-suite/vio
AgeCommit message (Collapse)Author
2016-02-19STM: Print/Extraction have to be skipped if -quickEnrico 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.
2015-01-09STM: fix handling of side effects in vio2voEnrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi