Notation variables are now taken into account as possible ltac bound variables

when internalizing a term.

1 files changed, 3 insertions, 1 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fde5a11f1..259690aa9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1551,8 +1551,10 @@ let internalize globalenv env allow_patvar lvar c =
         let solve = match solve with
         | None -> None
         | Some gen ->
-          let (cvars, lvars) = fst lvar in
+          let ((cvars, lvars), ntnvars) = lvar in
+          let ntnvars = Id.Map.domain ntnvars in
           let lvars = Id.Set.union lvars cvars in
+          let lvars = Id.Set.union lvars ntnvars in
           let ist = {
             Genintern.ltacvars = lvars;
             ltacrecvars = Id.Map.empty;