diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4f04b9fe1c..4c4c26f47e 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,7 +125,7 @@ module Make(T : Task) () = struct "-async-proofs-worker-priority"; CoqworkmgrApi.(string_of_priority priority)] (* Options to discard: 0 arguments *) - | "-emacs"::tl -> + | ("-emacs" | "--xml_format=Ppcmds" | "-batch") :: tl -> set_slave_opt tl (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" diff --git a/stm/stm.ml b/stm/stm.ml index f7d66b7b53..1c06c1efb7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2681,8 +2681,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtStartProof (guarantee, names) -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then - "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on." - |> Pp.str + "Nested proofs are discouraged and not allowed by default. \ + This error probably means that you forgot to close the last \"Proof.\" with \"Qed.\" or \"Defined.\". \ + If you really intended to use nested proofs, you can do so by turning the \"Nested Proofs Allowed\" flag on." + |> Pp.strbrk |> (fun s -> (UserError (None, s), Exninfo.null)) |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise |