From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 01:14:28 +0100 Subject: [api] Remove deprecated objects in engine / interp / library --- library/globnames.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'library/globnames.mli') diff --git a/library/globnames.mli b/library/globnames.mli index 2fe35ebcc..15fcd5bdd 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -49,10 +49,6 @@ val printable_constr_of_global : GlobRef.t -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t -(** Obsolete synonyms for constr_of_global and global_of_constr *) -val reference_of_constr : constr -> GlobRef.t -[@@ocaml.deprecated "Alias of Globnames.global_of_constr"] - module RefOrdered : sig type t = GlobRef.t val compare : t -> t -> int -- cgit v1.2.3