From fd186f119d5bb77bb2ece2c2591443c9140d673c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 6 Mar 2014 01:32:11 +0100
Subject: Fixing interpretation of tactics in terms. It was forgetting part of
 the environment.

---
 interp/constrintern.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a1faf95e2..48c9ca47a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1558,6 +1558,7 @@ let internalize globalenv env allow_patvar lvar c =
           let ntnvars = Id.Map.domain ntnvars in
           let lvars = Id.Set.union lvars cvars in
           let lvars = Id.Set.union lvars ntnvars in
+          let lvars = Id.Set.union lvars env.ids in
           let ist = {
             Genintern.ltacvars = lvars;
             ltacrecvars = Id.Map.empty;
-- 
cgit v1.2.3