diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacstate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c81a4abc1b..80b72225f0 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,7 +124,7 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end |