Commit 8b020d69 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix markdown formatting and improve the changes.

This commit also removes the mention of "any" becoming ghost, which did
not happen.
parent 4a782ded
:x: marks a potential source of incompatibility
Standard library
* set library revamped
- set.Fset
type `set` -> type `fset` and `choose` -> `pick`
- `appset.Appset` -> `set.SetApp` and `impset.Impset` -> `set.SetImp`
type `t` -> `set` and `.contents` -> `.to_fset`
`empty` -> `empty ()`
* the `set` library has been revamped :x:
- in `set.Fset`, type `set` becomes `fset`; `choose` becomes `pick`
- module `appset.Appset` becomes `set.SetApp`;
`impset.Impset` becomes `set.SetImp`
- in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
Tools
* why3prove counterexamples output is not JSON by default. To restore previous
behavior, pass the argument --json
* counterexamples given by `why3prove` are no longer printed using JSON
by default; pass option `--json` to restore the previous behavior
API
* function Call_provers.print_prover_result now takes an additional boolean
argument ~json_model which state if the counterexamples are printed with json
format :x:
* `Call_provers.print_prover_result` now takes an additional argument
`~json_model` to indicate whether counterexamples are printed using JSON :x:
Transformations
* Improvement of apply/rewrite in presence of let. Solve a bug that prevents
applying hypothesis with nested let-bindings :x:
* Adding arguments to transformations without arguments is now forbidden
(previously ignored):x:
* Fix crash of eliminate_unknown_types
* Giving too many arguments to a transformation do not display a popup anymore
* Fix behavior of induction_arg_ty_lex (now equivalent to induction_ty_lex)
* Add optional arguments to induction_arg_pr (containing what is to be
generalized in the induction). Also, fixing its behavior.
Counterexamples
* Improved display of counterexamples in Task view
* `apply`/`rewrite` behaves better in presence of `let`;
hypotheses with nested let-bindings can now be applied :x:
* passing arguments to argument-free transformations is now forbidden
(previously ignored) :x:
* passing too many arguments to a transformation does not display a popup anymore
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
IDE
* Added a checkbutton in preferences to disallow auto jumping to next unproved
goal
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
Version 1.2.0, February 11, 2019
--------------------------------
......@@ -47,7 +42,6 @@ Drivers
be replaced by `syntax literal` and/or `syntax function` :x:
Language
* the `any` expression is now always ghost :x:
* a syntactic sugar called "auto-dereference" is introduced, so as
to avoid, on simple programs, the heavy use of `(!)` character on
references; see details in Section A.1 of the manual
......
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