@@ -5,6 +5,8 @@ New in 0.9.16:
5* Importing a module no longer means it is automatically reexported. A new
5* Importing a module no longer means it is automatically reexported. A new
6 "public" modifier has been added to import statements, which will reexport
6 "public" modifier has been added to import statements, which will reexport
7 the names exported from that module.
7 the names exported from that module.
8+* Implemented @-patterns. A pattern of the form x@p on the left hand side
9+ matches p, with x in scope on the right hand side with value p.
8* A new tactic sourceLocation that fills the current hole with the current
10* A new tactic sourceLocation that fills the current hole with the current
9 source code span, if this information is available. If not, it raises an
11 source code span, if this information is available. If not, it raises an