aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 19:03:03 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 19:03:03 +0100
commited0c434a05a929a659e43aed80ab7c8179a7daa3 (patch)
treed486bf54f6bbfd6ace8dc9cea52b959699f88ebe /library
parentc571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (diff)
[api] Insert miscellaneous API deprecation back to core.
Diffstat (limited to 'library')
-rw-r--r--library/globnames.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/library/globnames.mli b/library/globnames.mli
index 5c484b391..2e0cd62db 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -47,6 +47,7 @@ val global_of_constr : constr -> global_reference
(** Obsolete synonyms for constr_of_global and global_of_constr *)
val reference_of_constr : constr -> global_reference
+[@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
module RefOrdered : sig
type t = global_reference