diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 22:12:55 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-30 17:50:37 +0200 |
commit | 64d663bc7de8bb21ec98c15ae5876f5d1b1f0b34 (patch) | |
tree | 1035797330c69ea00d2883a2a7732a573d345924 | |
parent | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (diff) |
[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`.
-rw-r--r-- | kernel/names.ml | 3 | ||||
-rw-r--r-- | kernel/names.mli | 3 |
2 files changed, 6 insertions, 0 deletions
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 = |