mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
Update CHANGELOG
This commit is contained in:
parent
94074a9835
commit
51febe053e
@ -2,6 +2,9 @@ New in 0.9.16:
|
||||
--------------
|
||||
* Inductive-inductive definitions are now supported (i.e. simultaneously
|
||||
defined types where one is indexed by the other.)
|
||||
* Importing a module no longer means it is automatically reexported. A new
|
||||
"public" modifier has been added to import statements, which will reexport
|
||||
the names exported from that module.
|
||||
* A new tactic sourceLocation that fills the current hole with the current
|
||||
source code span, if this information is available. If not, it raises an
|
||||
error.
|
||||
|
Loading…
Reference in New Issue
Block a user