diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index be65faf234..60c6c7bd67 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1100,16 +1100,6 @@ module GlobRef = struct end -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -(* Better to have it here that in closure, since used in grammar.cma *) -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t |