Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to interpretation scopes

8 files changed, 85 insertions, 9 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c03a5fee90..02db8f6aab 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))) =
@@ -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
diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v
new file mode 100644
index 0000000000..6ff394bca6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -0,0 +1,29 @@
+(* Checking that unrelated terms requiring some scope do not affect
+   the interpretation of tactic-in-term. The "Check" was failing with:
+   The term "Set" has type "Type" while it is expected to have type
+   "nat". *)
+
+Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing).
+Check bar2 (Set + Set) Set.
+
+(* Taking into account scopes in notations containing tactic-in-term *)
+
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope.
+Notation bar x := (x%foo) (only parsing).
+Notation baz x := ltac:(exact x%foo) (only parsing).
+Check bar (O ~~).
+Check baz (O ~~). (* Was failing *)
+
+(* This was reported as bug #8706 *)
+
+Declare Scope my_scope.
+Notation "@ a" := a%nat (at level 100, only parsing) : my_scope.
+Delimit Scope my_scope with my.
+
+Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
+Definition test := (& (@4))%my.
+
+(* Check inconsistent scopes *)
+Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).