Commit eb9e7a58 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Edit changelog

parent b05192f5
...@@ -35,6 +35,8 @@ Transformations ...@@ -35,6 +35,8 @@ Transformations
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is * `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards. allowed to further destruct afterwards.
`destruct` can also destruct `true` and `false`. `destruct` can also destruct `true` and `false`.
* decision procedures used for reflection now must be declared explicitly using
`meta reflection val <function_name>` :x:
IDE IDE
* display of counterexamples in the Task view has been improved * display of counterexamples in the Task view has been improved
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment