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.

7 files changed, 55 insertions, 8 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ac2f82e8ce..02db8f6aab 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2051,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           let (ltacvars, ntnvars) = lvar in
           (* Preventively declare notation variables in ltac as non-bindings *)
           Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
-          let ntnvars = Id.Map.domain ntnvars in
           let extra = ltacvars.ltac_extra in
+          (* We inform ltac that the interning vars and the notation vars are bound *)
+          (* but we could instead rely on the "intern_sign" *)
           let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
-          let lvars = Id.Set.union lvars ntnvars in
+          let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
           let ltacvars = Id.Set.union lvars env.ids in
+          (* Propagating enough information for mutual interning with tac-in-term *)
+          let intern_sign = {
+            Genintern.intern_ids = env.ids;
+            Genintern.notation_variable_status = ntnvars
+          } in
           let ist = {
             Genintern.genv = globalenv;
             ltacvars;
             extra;
+            intern_sign;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
@@ -2344,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
             ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
+let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+      { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
+  let tmp_scope = scope_of_type_kind sigma kind in
+  let impls = empty_internalization_env in
+  internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+    pattern_mode (ltacvars, vl) c
+
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
+  let ids = extract_ids env in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
-  let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
-						tmp_scope = None; scopes = []; impls = impls}
+  let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
     false (empty_ltac_sign, vl) a in
+  (* Splits variables into those that are binding, bound, or both *)
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a, reversible = notation_constr_of_glob_constr nenv c in
-  (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
   let unused = match reversible with NonInjective ids -> ids | _ -> [] in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index dd0944cc48..147a903fe2 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -185,6 +185,13 @@ val interp_notation_constr : env -> ?impls:internalization_env ->
   notation_interp_env -> constr_expr ->
   (bool * subscopes) Id.Map.t * notation_constr * reversibility_status
 
+(** Idem but to glob_constr (weaker check of binders) *)
+
+val intern_core : typing_constraint ->
+  env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+  Genintern.intern_variable_status -> constr_expr ->
+  glob_constr
+
 (** Globalization options *)
 val parsing_explicit : bool ref
 
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d9a0db040a..1b736b7977 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -14,16 +14,31 @@ open Genarg
 
 module Store = Store.Make ()
 
+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;
+}
+
+let empty_intern_sign = {
+  intern_ids = Id.Set.empty;
+  notation_variable_status = Id.Map.empty;
 }
 
 let empty_glob_sign env = {
   ltacvars = Id.Set.empty;
   genv = env;
   extra = Store.empty;
+  intern_sign = empty_intern_sign;
 }
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
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
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 3668455aeb..aa20bda705 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,8 +3,8 @@ Genredexpr
 Redops
 Tactypes
 Stdarg
-Genintern
 Notation_term
+Genintern
 Notation_ops
 Notation
 Syntax_def
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fcbcfae115..5e2a9af7e5 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -44,6 +44,7 @@ type glob_sign = Genintern.glob_sign = {
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   genv : Environ.env;
   extra : Genintern.Store.t;
+  intern_sign : Genintern.intern_variable_status;
 }
 
 let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
@@ -209,7 +210,7 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
+let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra; intern_sign} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let ltacvars = {
@@ -218,7 +219,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
     ltac_extra = extra;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c
+    warn (Constrintern.intern_core scope ~pattern_mode ~ltacvars env Evd.(from_env env) intern_sign) c
   in
   (c',if !strict_check then None else Some c)
 
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index a9f2d76e30..178f6af71d 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -21,6 +21,7 @@ type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
   genv : Environ.env;
   extra : Genintern.Store.t;
+  intern_sign : Genintern.intern_variable_status;
 }
 
 val make_empty_glob_sign : unit -> glob_sign