@@ -49,6 +49,10 @@ New in 0.9.18:
4949 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
5050 to reflect that if-notation makes sense with non-Bool datatypes.
5151* Agda-style semantic highlighting is supported over the IDE protocol.
52+* Experimental support for elaborator reflection. Users can now script the
53+ elaborator, for use in code generation and proof automation. This feature is
54+ still under rapid development and is subject to change without notice. See
55+ Language.Reflection.Elab and the %runElab constructs
5256
5357
5458New in 0.9.17: