diff options
Diffstat (limited to 'kernel')
| -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 = |