From 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 29 Oct 2020 13:59:45 +0100
Subject: 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.
---
 kernel/names.ml | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'kernel/names.ml')

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
-- 
cgit v1.2.3