[Agda] importing syntax declarations

[Benedict Kavanagh]

Hi,

I recently upgraded to 2.2.8. I am experimenting with the NotSoFresh 
Agda development by Pouillard/Pottier,
http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/
which uses the _:_ operator from Function.agda.

In file NotSoFresh/Lemmas.agda
----
.
.
open import Function using (_∘_;_∶_)
.
.
----

In Agda 2.2.8 the '_:_' operator for adding types to subexpressions is 
now a syntax declaration.
The above import complains that Function.agda does not export '_:_'.

Can anyone explain how syntax extensions interact with modules?
In particular can you hide them? Can you selectively import them?
If so is there a new agda syntax for importing syntax extensions?

Thanks,
-Ben




-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.