aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/stm.ml6
2 files changed, 4 insertions, 4 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 25f9d7c187..9c58df5b21 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -123,7 +123,7 @@ module Make(T : Task) = struct
"-worker-id"; name;
"-async-proofs-worker-priority";
Flags.string_of_priority !Flags.async_proofs_worker_priority]
- | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+ | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl
| ("-async-proofs" |"-toploop" |"-vio2vo"
|"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
|"-compile" |"-compile-verbose"
diff --git a/stm/stm.ml b/stm/stm.ml
index 7c96208546..3386044f26 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1133,7 +1133,7 @@ let record_pb_time ?loc proof_name time =
hints := Aux_file.set !hints proof_name proof_build_time
end
-exception RemoteException of Pp.std_ppcmds
+exception RemoteException of Pp.t
let _ = CErrors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
@@ -1274,7 +1274,7 @@ end = struct (* {{{ *)
type error = {
e_error_at : Stateid.t;
e_safe_id : Stateid.t;
- e_msg : Pp.std_ppcmds;
+ e_msg : Pp.t;
e_safe_states : Stateid.t list }
type response =
@@ -1711,7 +1711,7 @@ end = struct (* {{{ *)
type response =
| RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
- | RespError of Pp.std_ppcmds
+ | RespError of Pp.t
| RespNoProgress
let name = ref "tacworker"