@@ -2,6 +2,9 @@ New in 0.9.16:
22--------------
33* Inductive-inductive definitions are now supported (i.e. simultaneously
44 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.
58* A new tactic sourceLocation that fills the current hole with the current
69 source code span, if this information is available. If not, it raises an
710 error.