Merge PR #8972: Fix #4771: Substitution of inline global reference in tactics is broken

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