@@ -2,6 +2,9 @@ New in 0.9.16:
2--------------
2--------------
3* Inductive-inductive definitions are now supported (i.e. simultaneously
3* Inductive-inductive definitions are now supported (i.e. simultaneously
4 defined types where one is indexed by the other.)
4 defined types where one is indexed by the other.)
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
7+ the names exported from that module.
5* A new tactic sourceLocation that fills the current hole with the current
8* A new tactic sourceLocation that fills the current hole with the current
6 source code span, if this information is available. If not, it raises an
9 source code span, if this information is available. If not, it raises an