@@ -49,6 +49,10 @@ New in 0.9.18:
49 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
49 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
50 to reflect that if-notation makes sense with non-Bool datatypes.
50 to reflect that if-notation makes sense with non-Bool datatypes.
51* Agda-style semantic highlighting is supported over the IDE protocol.
51* 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
54New in 0.9.17:
58New in 0.9.17: