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 /kernel/names.ml | |
| 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`.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 3 |
1 files changed, 3 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 |