From bd9e68b11a9b7d6a9acb6bacb7ef169129e37a1b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Nov 2018 11:46:39 +0100
Subject: Fix #4771: Substitution of inline global reference in tactics is
 broken

---
 plugins/ltac/tacsubst.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3