From 9402b6efad32757f44d72d83f6aabdca8829e3ed Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 7 Nov 2017 00:48:14 +0100 Subject: [api] Remove 8.7 ML-deprecated functions. --- lib/flags.mli | 8 -------- 1 file changed, 8 deletions(-) (limited to 'lib/flags.mli') diff --git a/lib/flags.mli b/lib/flags.mli index 5233e72a2..0ff3e0a81 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -87,14 +87,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Deprecated *) -val make_silent : bool -> unit -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_silent : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_verbose : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] - (* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool -- cgit v1.2.3