diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.mli | 2 | ||||
| -rw-r--r-- | lib/feedback.mli | 7 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | lib/future.ml | 3 | ||||
| -rw-r--r-- | lib/future.mli | 7 | ||||
| -rw-r--r-- | lib/system.ml | 4 |
7 files changed, 4 insertions, 25 deletions
diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 60c8fb4449..b241fdc6cc 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t val aux_file_name_for : string -> string val start_aux_file : aux_file:string -> v_file:string -> unit -val stop_aux_file : unit -> unit +val stop_aux_file : unit -> unit val recording : unit -> bool val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit diff --git a/lib/feedback.mli b/lib/feedback.mli index dc8449ed71..5375d97d57 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -74,13 +74,8 @@ val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_conte (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit -(** {6 output functions} +(** {6 output functions} *) -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) diff --git a/lib/flags.ml b/lib/flags.ml index 190de5853d..f09dc48f5d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let record_aux_file = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 1c96796220..185a5f8425 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,10 +31,6 @@ (** Command-line flags *) -(** Set by coqtop to tell the kernel to output to the aux file; will - be eventually removed by cleanups such as PR#1103 *) -val record_aux_file : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index 01fb7d0297..d3ea538549 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -98,7 +98,6 @@ let peek_val kx = let _, _, _, x = get kx in match !x with let uuid kx = let _, id, _, _ = get kx in id let from_val ?(fix_exn=id) v = create fix_exn (Val v) -let from_here ?(fix_exn=id) v = create fix_exn (Val v) let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn @@ -168,8 +167,6 @@ let join kx = kx := Finished v; v -let sink kx = if is_val kx then ignore(join kx) - let split2 x = chain x (fun x -> fst x), chain x (fun x -> snd x) diff --git a/lib/future.mli b/lib/future.mli index 8e5f704837..c0fc91bcc3 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -55,10 +55,6 @@ val create : fix_exn -> (unit -> 'a) -> 'a computation argument should really be given *) val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation -(* Like from_val, but also takes a snapshot of the global state. Morally - the value is not just the 'a but also the global system state *) -val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation - (* To get the fix_exn of a computation and build a Lemmas.declaration_hook. * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the @@ -100,9 +96,6 @@ val compute : 'a computation -> 'a value * in a computation obtained by chaining on a joined future. *) val join : 'a computation -> 'a -(* Call this before stocking the future. If it is_val then it is joined *) -val sink : 'a computation -> unit - (*** Utility functions ************************************************* ***) val split2 : ('a * 'b) computation -> 'a computation * 'b computation diff --git a/lib/system.ml b/lib/system.ml index b1a9efccfc..8c333ec267 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -300,13 +300,13 @@ let with_time ~batch ~header f x = let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) |