From 64d663bc7de8bb21ec98c15ae5876f5d1b1f0b34 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 22:12:55 +0200 Subject: [api] Reintroduce `Names.global_reference` alias Due to a bad interaction between PRs, the `Names.global_reference` alias was removed in 8.9, where it should disappear in 8.10. The original PR #6156 deprecated the alias in `Libnames`. --- kernel/names.ml | 3 +++ kernel/names.mli | 3 +++ 2 files changed, 6 insertions(+) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 58d311dd5..1f2666a95 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -906,6 +906,9 @@ module GlobRef = struct end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t diff --git a/kernel/names.mli b/kernel/names.mli index 566fcd0f9..fdaa228fd 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -749,6 +749,9 @@ module GlobRef : sig end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = -- cgit v1.2.3