Agda-2.3.2.2: test/fail/Issue154.agda
-- The same name can not be exported more than once from a module. module Issue154 where module A where postulate X : Set module B where postulate X : Set open A public
-- The same name can not be exported more than once from a module. module Issue154 where module A where postulate X : Set module B where postulate X : Set open A public