diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ff4688480..7c5a3bc6a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1038,7 +1038,7 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - CErrors.user_err "undo_vernac_classifier" + CErrors.user_err ~hdr:"undo_vernac_classifier" (str "Cannot undo") end (* }}} *) @@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then - CErrors.user_err "STM" (str "Duplicate block delimiter " ++ str name); + CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name); proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters let mk_doc_node id = function @@ -1141,7 +1141,7 @@ let detect_proof_block id name = VCS.create_proof_block decl name end with Not_found -> - CErrors.user_err "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) @@ -1706,7 +1706,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.user_err "STM" (strbrk("the par: goal selector supports ground "^ + CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1719,7 +1719,7 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.user_err "STM" (str"The solution is not ground") + else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) @@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id = | _ -> assert false end with Not_found -> - CErrors.user_err "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) in @@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty = let snapshot_vio ldir long_f_dot_vo = finish (); if List.length (VCS.branches ()) > 1 then - CErrors.user_err "stm" (str"Cannot dump a vio with open proofs"); + CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo (Global.opaque_tables ()) |