From a023009ba68c70d8654b29bd2f68631cc5536ba9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Sep 2020 18:09:25 +0200 Subject: [stm] move par: implementation to vernac/comTactic and stm/partac The current implementation of par: is still in the STM, but is optional. If the STM does not take over it, it defaults to the implementation of in comTactic which is based on all: (i.e. sequential). This commit also moved the interpretation of a tactic from g_ltac to vernac/comTactic which is more appropriate. Co-authored-by: Gaëtan Gilbert --- topbin/coqtacticworker_bin.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'topbin') diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml index 252c8faa05..706554e025 100644 --- a/topbin/coqtacticworker_bin.ml +++ b/topbin/coqtacticworker_bin.ml @@ -8,6 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () +module W = AsyncTaskQueue.MakeWorker(Partac.TacTask) () let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker" -- cgit v1.2.3