Tactic mode "escapes" sections for sections within namespaces

[bmsherman]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Consider the following code:

namespace foo
section
parameter x : ℕ

def my_x : ℕ := x

lemma bar : my_x = my_x + 0
  := nat.add_zero my_x

lemma bar' : my_x = my_x + 0
:= begin apply (nat.add_zero my_x) end --error on this line

end
end foo

Actual behavior: Definition of bar' fails with the error

type mismatch at application
  nat.add_zero my_x
term
  my_x
has type
  ℕ → ℕ
but is expected to have type
  ℕ
state:
x : ℕ
⊢ my_x = my_x + 0

What is happening is that inside the tactic mode, the environment is behaving as if it were outside the section, and thus my_x takes an argument corresponding to the parameter x. If one removes the lines namespace foo and end foo, so that the section is no longer within a namespace, then the definition of bar' works.

Expected behavior: The environment should behave similarly in tactic mode as outside of tactic mode. That is, it should behave as it does behave for sections that are not within namespaces.

Versions

Lean HEAD from July 21, 2017, Lean (version 3.2.1, commit 667e1e1, Release)

[gebner]

The problem is that the my_x alias for my_x x is stored in the parser right now. A fix for this will probably have to wait until we implement #1674.