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(-)

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


From ccefe52e6cb755da9470ef1fe707d570a26681cb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Nov 2018 11:47:57 +0100
Subject: Test case for #4771: Substitution of inline global reference in
 tactics is broken

---
 test-suite/bugs/closed/bug_4771.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_4771.v

diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v
new file mode 100644
index 0000000000..e25e5a1be5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4771.v
@@ -0,0 +1,21 @@
+(* The following code used to trigger an anomaly in functor substitutions *)
+
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
-- 
cgit v1.2.3