diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /kernel/names.mli | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
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 |