aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml30
-rw-r--r--ide/ideutils.ml2
-rw-r--r--ide/minilib.ml6
-rw-r--r--ide/minilib.mli3
-rw-r--r--lib/pp.ml2
-rw-r--r--lib/pp.mli3
-rw-r--r--library/summary.ml6
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--proofs/proof_using.ml2
-rw-r--r--stm/asyncTaskQueue.ml25
-rw-r--r--stm/stm.ml58
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/vernacentries.ml4
13 files changed, 81 insertions, 68 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index cee243f91..1b4c5d3be 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -128,6 +128,9 @@ end = struct
end
open SentenceId
+let log_pp msg : unit task =
+ Coq.lift (fun () -> Minilib.log_pp msg)
+
let log msg : unit task =
Coq.lift (fun () -> Minilib.log msg)
@@ -308,7 +311,7 @@ object(self)
method private print_stack =
Minilib.log "document:";
- Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
+ Minilib.log_pp (Doc.print document (dbg_to_string buffer))
method private enter_focus start stop =
let at id id' _ = Stateid.equal id' id in
@@ -379,8 +382,7 @@ object(self)
Coq.bind (Coq.seq action query) next
method private mark_as_needed sentence =
- Minilib.log("Marking " ^
- Pp.string_of_ppcmds (dbg_to_string buffer false None sentence));
+ Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
let to_process = Tags.Script.to_process in
@@ -437,9 +439,11 @@ object(self)
| _ -> None in
try Some (Doc.find_map document finder)
with Not_found -> None in
- let log s state_id =
- Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
- (Option.default Stateid.dummy state_id)) in
+ let log_pp s state_id =
+ Minilib.log_pp Pp.(seq
+ [str "Feedback "; s; str " on ";
+ str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
+ let log s state_id = log_pp (Pp.str s) state_id in
begin match msg.contents, sentence with
| AddedAxiom, Some (id,sentence) ->
log "AddedAxiom" id;
@@ -469,24 +473,24 @@ object(self)
(Printf.sprintf "%s %s %s" filepath ident ty)
| Message(Error, loc, msg), Some (id,sentence) ->
let loc = Option.default Loc.ghost loc in
- let msg = Pp.string_of_ppcmds msg in
- log "ErrorMsg" id;
+ log_pp Pp.(str "ErrorMsg" ++ msg) id;
remove_flag sentence `PROCESSING;
- add_flag sentence (`ERROR (loc, msg));
+ let rmsg = Pp.string_of_ppcmds msg in
+ add_flag sentence (`ERROR (loc, rmsg));
self#mark_as_needed sentence;
- self#attach_tooltip sentence loc msg;
+ self#attach_tooltip sentence loc rmsg;
if not (Loc.is_ghost loc) then
self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
| Message(Warning, loc, msg), Some (id,sentence) ->
let loc = Option.default Loc.ghost loc in
- let rmsg = Pp.string_of_ppcmds msg in
- log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id;
+ log_pp Pp.(str "WarningMsg" ++ msg) id;
+ let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`WARNING (loc, rmsg));
self#attach_tooltip sentence loc rmsg;
self#position_warning_tag_at_sentence sentence loc;
messages#push Warning msg
| Message(lvl, loc, msg), Some (id,sentence) ->
- log ("Msg: " ^ Pp.string_of_ppcmds msg) id;
+ log_pp Pp.(str "Msg" ++ msg) id;
messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 101f1a5ee..da867e689 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -337,7 +337,7 @@ let default_logger level message =
| Feedback.Warning -> `WARNING
| Feedback.Error -> `ERROR
in
- Minilib.log ~level (Pp.string_of_ppcmds message)
+ Minilib.log_pp ~level message
(** {6 File operations} *)
diff --git a/ide/minilib.ml b/ide/minilib.ml
index d11e8c56b..2c24e46f8 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -30,7 +30,7 @@ let debug = ref false
print in the response buffer.
*)
-let log ?(level = `DEBUG) msg =
+let log_pp ?(level = `DEBUG) msg =
let prefix = match level with
| `DEBUG -> "DEBUG"
| `INFO -> "INFO"
@@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg =
| `FATAL -> "FATAL"
in
if !debug then begin
- try Printf.eprintf "[%s] %s\n%!" prefix msg
+ try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg
with _ -> ()
end
+let log ?level str = log_pp ?level (Pp.str str)
+
let coqify d = Filename.concat d "coq"
let coqide_config_home () =
diff --git a/ide/minilib.mli b/ide/minilib.mli
index b7672c900..4517a2374 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,7 +22,8 @@ type level = [
(** debug printing *)
val debug : bool ref
-val log : ?level:level -> string -> unit
+val log_pp : ?level:level -> Pp.std_ppcmds -> unit
+val log : ?level:level -> string -> unit
val coqide_config_home : unit -> string
val coqide_config_dirs : unit -> string list
diff --git a/lib/pp.ml b/lib/pp.ml
index 7b21f9bbd..80c599274 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with
| s, Ppcmd_empty -> s
| s1, s2 -> Ppcmd_glue [s1; s2]
+let seq s = Ppcmd_glue s
+
let (++) = app
(* formatting commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 2c45ce0a7..4b7ac5c1a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -68,6 +68,9 @@ val comment : string list -> std_ppcmds
val app : std_ppcmds -> std_ppcmds -> std_ppcmds
(** Concatenation. *)
+val seq : std_ppcmds list -> std_ppcmds
+(** Multi-Concatenation. *)
+
val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
(** Infix alias for [app]. *)
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f38..2ec4760d6 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
try fold id decl state
with e when CErrors.noncritical e ->
let e = CErrors.push e in
- Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
- (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
+ Feedback.msg_error
+ Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+ str (name_of_summary id);
+ CErrors.iprint e]);
iraise e
in
(** We rely on the order of the frozen list, and the order of folding *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 120cde5e5..ca7330fdb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -195,9 +195,9 @@ let check_no_pending_proof () =
if not (there_are_pending_proofs ()) then
()
else begin
- CErrors.error (Pp.string_of_ppcmds
+ CErrors.user_err
(str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
- str"Use \"Abort All\" first or complete proof(s)."))
+ str"Use \"Abort All\" first or complete proof(s).")
end
let discard_gen id =
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a125fb10d..f51586c73 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids =
let suggest_Proof_using name env vars ids_typ context_ids =
let module S = Id.Set in
let open Pp in
- let print x = prerr_endline (string_of_ppcmds x) in
+ let print x = Feedback.msg_error x in
let pr_set parens s =
let wrap ppcmds =
if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 28548ecee..125491988 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,9 +10,9 @@ open CErrors
open Pp
open Util
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
type 'a worker_status = [ `Fresh | `Old of 'a ]
@@ -147,23 +147,23 @@ module Make(T : Task) = struct
let stop_waiting = ref false in
let expiration_date = ref (ref false) in
let pick_task () =
- prerr_endline "waiting for a task";
+ stm_prerr_endline "waiting for a task";
let pick age (t, c) = not !c && T.task_match age t in
let task, task_expiration =
TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
expiration_date := task_expiration;
last_task := Some task;
- prerr_endline ("got task: "^T.name_of_task task);
+ stm_prerr_endline ("got task: " ^ T.name_of_task task);
task in
let add_tasks l =
List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
let get_exec_token () =
ignore(CoqworkmgrApi.get 1);
got_token := true;
- prerr_endline ("got execution token") in
+ stm_prerr_endline ("got execution token") in
let kill proc =
Worker.kill proc;
- prerr_endline ("Worker exited: " ^
+ stm_prerr_endline ("Worker exited: " ^
match Worker.wait proc with
| Unix.WEXITED 0x400 -> "exit code unavailable"
| Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
report_status ~id "Idle";
let task = pick_task () in
match T.request_of_task !worker_age task with
- | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+ | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
| Some req ->
try
get_exec_token ();
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
raise e (* we pass the exception to the external handler *)
| MarshalError s -> T.on_marshal_error s task; raise Die
| e ->
- pr_err ("Uncaught exception in worker manager: "^
- string_of_ppcmds (print e));
+ stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
flush_all (); raise Die
done with
| (Die | TQueue.BeingDestroyed) ->
@@ -261,7 +260,7 @@ module Make(T : Task) = struct
let broadcast { queue } = TQueue.broadcast queue
let enqueue_task { queue; active } (t, _ as item) =
- prerr_endline ("Enqueue task "^T.name_of_task t);
+ stm_prerr_endline ("Enqueue task "^T.name_of_task t);
TQueue.push queue item
let cancel_worker { active } n = Pool.cancel n active
@@ -329,11 +328,11 @@ module Make(T : Task) = struct
CEphemeron.clear ()
with
| MarshalError s ->
- pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+ stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
| End_of_file ->
- prerr_endline "connection lost"; flush_all (); exit 2
+ stm_prerr_endline "connection lost"; flush_all (); exit 2
| e ->
- pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+ stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
flush_all (); exit 1
done
diff --git a/stm/stm.ml b/stm/stm.ml
index 75872d633..ee142b293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,10 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
open Vernacexpr
open CErrors
@@ -540,7 +540,7 @@ end = struct (* {{{ *)
let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
- prerr_endline (fun () -> "mode:" ^ mode);
+ stm_prerr_endline (fun () -> "mode:" ^ mode);
Proof_global.activate_proof_mode mode
with Failure _ ->
checkout Branch.master;
@@ -852,7 +852,7 @@ end = struct (* {{{ *)
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
try
- prerr_endline (fun () -> "defining "^str_id^" (cache="^
+ stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
@@ -860,7 +860,7 @@ end = struct (* {{{ *)
fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
- prerr_endline (fun () -> "setting cur id to "^str_id);
+ stm_prerr_endline (fun () -> "setting cur id to "^str_id);
cur_id := id;
if feedback_processed then
Hooks.(call state_computed id ~in_cache:false);
@@ -994,11 +994,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
in
let aux_interp cmd =
if is_filtered_command cmd then
- prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+ stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
else match cmd with
| VernacShow ShowScript -> ShowScript.show_script ()
| expr ->
- prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+ stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
with e ->
let e = CErrors.push e in
@@ -1431,8 +1431,8 @@ end = struct (* {{{ *)
| Some (safe, err) -> err, safe
| None -> Stateid.dummy, Stateid.dummy in
let e_msg = iprint (e, info) in
- prerr_endline (fun () -> "failed with the following exception:");
- prerr_endline (fun () -> string_of_ppcmds e_msg);
+ stm_prerr_endline (fun () -> "failed with the following exception:");
+ stm_prerr_endline (fun () -> string_of_ppcmds e_msg);
let e_safe_states = List.filter State.is_cached_and_valid my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
@@ -1697,7 +1697,7 @@ end = struct (* {{{ *)
| Some (ReqBuildProof (r, b, _)) -> Some(r, b)
| _ -> None)
tasks in
- prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+ stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
reqs
let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1781,7 +1781,7 @@ end = struct (* {{{ *)
`Stay ((),[])
let on_marshal_error err { t_name } =
- pr_err ("Fatal marshal error: " ^ t_name );
+ stm_pr_err ("Fatal marshal error: " ^ t_name );
flush_all (); exit 1
let on_task_cancellation_or_expiration_or_slave_death = function
@@ -1880,7 +1880,7 @@ end = struct (* {{{ *)
let open Notations in
try
let pt, uc = Future.join f in
- prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+ stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
str"uc=" ++ Evd.pr_evar_universe_context uc)));
@@ -1925,7 +1925,7 @@ end = struct (* {{{ *)
let use_response _ _ _ = `End
let on_marshal_error _ _ =
- pr_err ("Fatal marshal error in query");
+ stm_pr_err ("Fatal marshal error in query");
flush_all (); exit 1
let on_task_cancellation_or_expiration_or_slave_death _ = ()
@@ -2000,7 +2000,7 @@ let warn_deprecated_nested_proofs =
"stop working in a future Coq version"))
let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
let name = function
| [] -> no_name
@@ -2100,7 +2100,7 @@ let string_of_reason = function
| `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
| `Unknown -> "unsupported case"
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
let log_processing_async id name = log_string Printf.(sprintf
"%s: proof %s: asynch" (Stateid.to_string id) name
)
@@ -2187,16 +2187,16 @@ let known_state ?(redefine_qed=false) ~cache id =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
- prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
reach ~safe_id id;
cherry_pick_non_pstate ()) id
(* traverses the dag backward from nodes being already calculated *)
and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
- prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
if not redefine_qed && State.is_cached ~cache id then begin
Hooks.(call state_computed id ~in_cache:true);
- prerr_endline (fun () -> "reached (cache)");
+ stm_prerr_endline (fun () -> "reached (cache)");
State.install_cached id
end else
let step, cache_step, feedback_processed =
@@ -2348,7 +2348,7 @@ let known_state ?(redefine_qed=false) ~cache id =
else cache_step in
State.define ?safe_id
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
- prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+ stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
end (* }}} *)
@@ -2363,7 +2363,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline (fun () -> "Initializing workers");
+ stm_prerr_endline (fun () -> "Initializing workers");
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []
@@ -2415,9 +2415,9 @@ let rec join_admitted_proofs id =
let join () =
finish ();
wait ();
- prerr_endline (fun () -> "Joining the environment");
+ stm_prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
- prerr_endline (fun () -> "Joining Admitted proofs");
+ stm_prerr_endline (fun () -> "Joining Admitted proofs");
join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
VCS.print ();
VCS.print ()
@@ -2491,7 +2491,7 @@ let handle_failure (e, info) vcs tty =
anomaly(str"error with no safe_id attached:" ++ spc() ++
CErrors.iprint_no_report (e, info))
| Some (safe_id, id) ->
- prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
if tty && interactive () = `Yes then begin
(* We stay on a valid state *)
@@ -2514,13 +2514,13 @@ let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
let process_transaction ?(newtip=Stateid.fresh ()) ~tty
({ verbose; loc; expr } as x) c =
- prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+ stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
let vcs = VCS.backup () in
try
let head = VCS.current_branch () in
VCS.checkout head;
let rc = begin
- prerr_endline (fun () ->
+ stm_prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
(* PG stuff *)
@@ -2558,7 +2558,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtStm (VtBack id, false), VtNow ->
- prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2708,7 +2708,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
expr = VernacShow (ShowGoal OpenSubgoals) }
| _ -> ()
end;
- prerr_endline (fun () -> "processed }}}");
+ stm_prerr_endline (fun () -> "processed }}}");
VCS.print ();
rc
with e ->
@@ -2894,7 +2894,7 @@ let edit_at id =
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
CErrors.print_no_report e)
| Some (_, id) ->
- prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
VCS.print ();
iraise (e, info)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e944..6d71601cc 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with Not_found ->
(* spiwack: the format of this error message should probably
be improved. *)
- let err_msg = string_of_ppcmds
+ let err_msg =
(str "boolean->Leibniz:" ++
str "You have to declare the" ++
str "decidability over " ++
Printer.pr_constr tt1 ++
str " first.")
in
- error err_msg
+ user_err err_msg
in let bl_args =
Array.append (Array.append
(Array.map (fun x -> x) v)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 09c43f93e..999fe297e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,7 +39,7 @@ module NamedDecl = Context.Named.Declaration
let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
let debug = false
-let prerr_endline x =
+let vernac_prerr_endline x =
if debug then prerr_endline (x ()) else ()
(* Misc *)
@@ -1933,7 +1933,7 @@ let vernac_load interp fname =
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
let interp ?proof ~loc locality poly c =
- prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+ vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
match c with
(* The below vernac are candidates for removal from the main type
and to be put into a new doc_command datatype: *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 14:49:34 +0000