diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4626378db6..9173e23b89 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -88,20 +88,9 @@ let subst_reference subst = (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as Print. It is also used for non-evaluable references. *) -open Pp -open Printer let subst_global_reference subst = - let subst_global ref = - let ref',t' = subst_global subst ref in - if not (is_global ref' t') then - (let sigma, env = Pfedit.get_current_context () in - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ - pr_global ref')); - ref' - in - subst_or_var (subst_located subst_global) + subst_or_var (subst_located (subst_global_reference subst)) let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in |