diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /kernel/mod_subst.mli | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
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.
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 8 |
1 files changed, 0 insertions, 8 deletions
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 |