3 files changed, 15 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4e217b2cd..18d6c1a5b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       let arg = match arg with
       | None -> None
       | Some arg ->
-        let mk_env (c, (tmp_scope, subscopes)) =
+        let mk_env id (c, (tmp_scope, subscopes)) map =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
-          let gc = intern nenv c in
-          (gc, Some c)
+          try
+            let gc = intern nenv c in
+            Id.Map.add id (gc, Some c) map
+          with GlobalizationError _ -> map
         in
         let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
@@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
             | [pat] -> (glob_constr_of_cases_pattern pat, None)
             | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
-        let terms = Id.Map.map mk_env terms in
+        let terms = Id.Map.fold mk_env terms Id.Map.empty in
         let binders = Id.Map.map mk_env' binders in
         let bindings = Id.Map.fold Id.Map.add terms binders in
         Some (Genintern.generic_substitute_notation bindings arg)
diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v
new file mode 100644
index 000000000..a20ad1b4d
--- /dev/null
+++ b/test-suite/bugs/closed/5696.v
@@ -0,0 +1,5 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e)
+..)) (at level 200, x binder, y binder, e at level 220).
+Check (var2 a = 1; a).
diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v
new file mode 100644
index 000000000..55c7ee99a
--- /dev/null
+++ b/test-suite/bugs/closed/7903.v
@@ -0,0 +1,4 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
+Check bar x (x + x).