From 5d5fd2da5070d214c1f5bdb09976b9554c3965ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Nov 2014 10:07:16 -0800
Subject: [PATCH] fix(frontends/lean): tactic + section variables, fixes #332

---
 src/frontends/lean/util.cpp  | 25 +++++++++++++++++++++----
 tests/lean/run/issue332.lean | 11 +++++++++++
 tests/lean/run/tactic29.lean |  1 +
 3 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/issue332.lean

diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index e575a4f4f5..5f83656e87 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/explicit.h"
 #include "library/placeholder.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 
@@ -76,17 +77,33 @@ levels collect_local_nonvar_levels(parser & p, level_param_names const & ls) {
     return to_list(section_ls_buffer.begin(), section_ls_buffer.end());
 }
 
+// Version of collect_locals(expr const & e, expr_struct_set & ls) that ignores local constants occurring in
+// tactics.
+static void collect_locals_ignoring_tactics(expr const & e, expr_struct_set & ls) {
+    if (!has_local(e))
+        return;
+    for_each(e, [&](expr const & e, unsigned) {
+            if (!has_local(e))
+                return false;
+            if (is_by(e))
+                return false; // do not visit children
+            if (is_local(e))
+                ls.insert(e);
+            return true;
+        });
+}
+
 // Collect local constants occurring in type and value, sort them, and store in ctx_ps
 void collect_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & ctx_ps) {
     expr_struct_set ls;
     buffer<expr> include_vars;
     p.get_include_variables(include_vars);
     for (expr const & param : include_vars) {
-        collect_locals(mlocal_type(param), ls);
+        collect_locals_ignoring_tactics(mlocal_type(param), ls);
         ls.insert(param);
     }
-    collect_locals(type, ls);
-    collect_locals(value, ls);
+    collect_locals_ignoring_tactics(type, ls);
+    collect_locals_ignoring_tactics(value, ls);
     sort_locals(ls, p, ctx_ps);
 }
 
@@ -110,7 +127,7 @@ levels remove_local_vars(parser const & p, levels const & ls) {
 
 list<expr> locals_to_context(expr const & e, parser const & p) {
     expr_struct_set ls;
-    collect_locals(e, ls);
+    collect_locals_ignoring_tactics(e, ls);
     buffer<expr> locals;
     sort_locals(ls, p, locals);
     std::reverse(locals.begin(), locals.end());
diff --git a/tests/lean/run/issue332.lean b/tests/lean/run/issue332.lean
new file mode 100644
index 0000000000..bcf5114aff
--- /dev/null
+++ b/tests/lean/run/issue332.lean
@@ -0,0 +1,11 @@
+import tools.tactic logic.eq
+variable {a : Type}
+
+definition foo {A : Type} : A → A :=
+begin
+intro a, exact a
+end
+check @foo
+
+example : foo 10 = 10 :=
+rfl
diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean
index f557c4179f..7a3644545e 100644
--- a/tests/lean/run/tactic29.lean
+++ b/tests/lean/run/tactic29.lean
@@ -11,6 +11,7 @@ section
   check H1
   check H
   check H2
+  include H
   theorem test : a = b ∧ a = a
   := by apply and.intro; apply H; apply eq.refl
 end