diff options
| author | coqbot-app[bot] | 2020-12-30 17:45:17 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-30 17:45:17 +0000 |
| commit | d6331216fd8f5e655ab525677ef1e1af634327b5 (patch) | |
| tree | 383aaaf1243605e401703dada18ef5425403967b /kernel/mod_subst.ml | |
| parent | d338a65ce7c4619ecc238c091a409175f5330d8f (diff) | |
| parent | 1be5dccd25d36393a39b5ec28784f4b52c643080 (diff) | |
Merge PR #13321: Move evaluable_global_reference from Names to Tacred.
Reviewed-by: herbelin
Ack-by: ejgallego
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 9 |
1 files changed, 0 insertions, 9 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 |