From db33ec1898dacbcd398c38e0a6535be931ed5fb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 22 Dec 2013 15:38:25 +0100
Subject: Notation variables are now taken into account as possible ltac bound
 variables when internalizing a term.

---
 interp/constrintern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fde5a11f15..259690aa97 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;
-- 
cgit v1.2.3