Fixes rest of #3468 (tactic-in-term was not respecting scopes).

We do it by passing interning env to ltac interning.

Collecting scopes was already done by side-effect internally to
Constrintern. We expose the side-effect to ltac.

1 files changed, 9 insertions, 0 deletions

diff --git a/interp/genintern.mli b/interp/genintern.mli
index f4f064bcac..4100f39029 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -14,10 +14,19 @@ open Genarg
 
 module Store : Store.S
 
+type intern_variable_status = {
+  intern_ids : Id.Set.t;
+  notation_variable_status :
+    (bool ref * Notation_term.subscopes option ref *
+       Notation_term.notation_var_internalization_type)
+      Id.Map.t
+}
+
 type glob_sign = {
   ltacvars : Id.Set.t;
   genv : Environ.env;
   extra : Store.t;
+  intern_sign : intern_variable_status;
 }
 
 val empty_glob_sign : Environ.env -> glob_sign