Merge PR #13321: Move evaluable_global_reference from Names to Tacred.

Reviewed-by: herbelin
Ack-by: ejgallego

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