From ba110aab290cecc8847f3bc3b8396d5d1b9493b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Oct 2018 15:28:35 +0200
Subject: Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated
 scopes).

We compute the binding to tactic-in-term once for all in the right
scopes before interpreting the tactic.

An alternative would have been to surround the constr_expr by
CDelimiters to simulate its interpretation in the expected scopes
(though this would not have worked for temporary scopes).
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c03a5fee90..ac2f82e8ce 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -737,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
           try
             let gc = intern nenv c in
-            Id.Map.add id (gc, Some c) map
+            Id.Map.add id (gc, None) map
           with Nametab.GlobalizationError _ -> map
         in
         let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
-- 
cgit v1.2.3