20070619-1

a should be in scope after B' has been opened:

  module Bug where

  module A where
    postulate a : Set

  module B (b : Set) where
    open A public

  module C where
    postulate c : Set

    module B' = B c
    open B'

    d : Set
    d = a

Error message:

  Bug.agda:16,7-8
  Not in scope:
    a at Bug.agda:16,7-8
  when scope checking a

Fixed.

Page last modified on October 16, 2007, at 09:38 am
Powered by PmWiki