Commit c6ebb4ab authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update changes.

parent bed36a37
:x: marks a potential source of incompatibility
Session
* file path stored in session files are now represented in an
system-independent way, so as to work for example under exotic OS
like MS-windows
* file path stored in session files are now represented in a
system-independent way
Drivers
* the clause `syntax converter` disappeared. Any former use should
* the clause `syntax converter` has been removed; any former use should
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
* 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.
references; see details in Section A.1 of the manual
Transformations
* `split_vc` and `subst_all` now avoid substituting user symbols by
......@@ -21,7 +20,7 @@ Transformations
* `destruct_rec` applies `destruct` recursively on a goal
* `destruct` now simplifies away equalities on constructors :x:
* `destruct` now simplifies `if .. then .. else ..` and `match .. with ..` :x:
* `destruct_alg` renamed to `destruct_term`. It also has a new experimental
* `destruct_alg` renamed to `destruct_term`; it also has a new experimental
keyword `using` to name newly destructed elements :x:
Tools
......@@ -38,12 +37,21 @@ IDE
* added support for GTK3
Counterexamples
* Changed the way counterexamples are triggered. Read Section 5.3.7
* the trigger for counterexamples has been changed; read Section 5.3.7
of the manual for details :x:
* various improvements on the generated counterexamples
* Field names now use ident names instead of smt generated ones, e.g.
int32qtint -> int32'int :x:
* Fix parsing of bitvector values from counterexamples generated by Z3
* field names now use ident names instead of smt generated ones, e.g.,
`int32qtint` -> `int32'int` :x:
* fixed parsing of bitvector values from counterexamples generated by Z3
Extraction
* fixed extraction of functions passed as arguments
* fixed extraction of recursive polymorphic functions for Ocaml
* improved extraction of records for C
Standard library
* `Stack.length` and `Queue.length` now return a `Peano.t`, for
improved extraction :x:
Provers
* support for Z3 4.8.1 (released Oct 16, 2018)
......
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