Names not displayed properly when open public is used

[GoogleCodeExporter]

-- Define the following three modules:

module A where

postulate A : Set

module B where

open import A public

module C where

open import B

test : A -> Set
test x = ?

-- Show the environment in the scope of the meta-variable. You get the
-- following:
--
-- x : .A.A
--
-- It would be nice if the output had been
--
-- x : A
--
-- instead, since A is actually in scope.

Original issue reported on code.google.com by nils.anders.danielsson on 1 May 2008 at 2:08

[GoogleCodeExporter]

Uh, me too!

Original comment by naesten on 9 May 2008 at 2:39

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 18 Jun 2008 at 8:48

• Changed state: Accepted

[GoogleCodeExporter]

This is by far the oldest issue which is not low priority. Any progress?

Original comment by nils.anders.danielsson on 15 Apr 2009 at 6:03

[GoogleCodeExporter]

Yes

Original comment by ulf.nor...@gmail.com on 22 Apr 2009 at 2:03

• Changed state: Fixed