diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 747299bb12..09885396c0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -714,14 +714,6 @@ module GlobRef : sig end -(** Better to have it here that in Closure, since required in grammar.cma *) -(* XXX: Move to a module *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t |