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.

4 files changed, 0 insertions, 35 deletions

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
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index bc5816dafb..9cf270cff7 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -146,14 +146,6 @@ val subst_proj : substitution -> Projection.t -> Projection.t
 
 val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action
 
-(** 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). *)
-val subst_evaluable_reference :
-  substitution -> evaluable_global_reference -> evaluable_global_reference
-
 (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
 val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
 
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
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