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 --- stm/asyncTaskQueue.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index a8088dae36..4f04b9fe1c 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -386,3 +386,8 @@ end module MakeQueue(T : Task) () = struct include Make(T) () end module MakeWorker(T : Task) () = struct include Make(T) () end + +exception RemoteException of Pp.t +let _ = CErrors.register_handler (function + | RemoteException ppcmd -> Some ppcmd + | _ -> None) -- cgit v1.2.3