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/mod_subst.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 2aeb1ea202..4778bf1121 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -340,15 +340,6 @@ let subst_retro_action subst action =
     let c' = subst_constant subst c in
     if c == c' then action else Register_type(prim, c')
 
-(* Here the semantics is completely unclear.
-   What does "Hint Unfold t" means when "t" is a parameter?
-   Does the user mean "Unfold X.t" or does she mean "Unfold y"
-   where X.t is later on instantiated with y? I choose the first
-   interpretation (i.e. an evaluable reference is never expanded). *)
-let subst_evaluable_reference subst = function
-  | EvalVarRef id -> EvalVarRef id
-  | EvalConstRef kn -> EvalConstRef (subst_constant subst kn)
-
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind c with
-- 
cgit v1.2.3