diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-07 00:48:14 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-07 00:53:19 +0100 |
commit | 9402b6efad32757f44d72d83f6aabdca8829e3ed (patch) | |
tree | 0ab9fc18568664e4b7bd0a63f9b52c6303e73a61 /lib | |
parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) |
[api] Remove 8.7 ML-deprecated functions.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cErrors.ml | 5 | ||||
-rw-r--r-- | lib/cErrors.mli | 11 | ||||
-rw-r--r-- | lib/flags.ml | 4 | ||||
-rw-r--r-- | lib/flags.mli | 8 | ||||
-rw-r--r-- | lib/loc.ml | 6 | ||||
-rw-r--r-- | lib/loc.mli | 11 |
6 files changed, 0 insertions, 45 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3f4e8aa12..94357aad3 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -137,8 +137,3 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false - -(* Deprecated functions *) -let error string = user_err (str string) -let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg -let errorlabstrm hdr msg = user_err ~hdr msg diff --git a/lib/cErrors.mli b/lib/cErrors.mli index f3253979f..6fcc97a91 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -93,14 +93,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Deprecated functions *) -val error : string -> 'a - [@@ocaml.deprecated "use [user_err] instead"] - -val errorlabstrm : string -> Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~hdr] instead"] - -val user_err_loc : Loc.t * string * Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~loc] instead"] - diff --git a/lib/flags.ml b/lib/flags.ml index a53a866ab..323b5492d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -140,10 +140,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let make_silent flag = quiet := flag -let is_silent () = !quiet -let is_verbose () = not !quiet - let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = !auto_intros 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 diff --git a/lib/loc.ml b/lib/loc.ml index 4a935a9d9..2cf4d3960 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -84,9 +84,3 @@ let raise ?loc e = let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) -(** Deprecated *) -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - - diff --git a/lib/loc.mli b/lib/loc.mli index fde490cc8..800940f21 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -65,14 +65,3 @@ val tag : ?loc:t -> 'a -> 'a located val map : ('a -> 'b) -> 'a located -> 'b located (** Modify an object carrying a location *) - -(** Deprecated functions *) -val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a - [@@ocaml.deprecated "use pattern matching"] - -val down_located : ('a -> 'b) -> 'a located -> 'b - [@@ocaml.deprecated "use pattern matching"] - -val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit - [@@ocaml.deprecated "use pattern matching"] - |