Commit bd5c75f7 authored by MARCHE Claude's avatar MARCHE Claude

release 0.81

parent 36813adc
* marks an incompatible change
version 0.81, March ??, 2013
version 0.81, March 25, 2013
==========================
o [prover] experimental support for SPASS >= 3.8 (with types)
......
......@@ -78,6 +78,18 @@ scheduled on March 2013
== New Features to announce ==
o [logic] accept type expressions in clone substitutions
o [whyml] support for relation chains (e.g., "e1 = e2 < e3")
* [whyml] every exception raised in a function must be listed
in as "raises { ... }" clause. A postcondition may be omitted
and equals to "true" by default.
* [whyml] if a function definition contains a "writes { ... }"
clause, then every write effect must be listed. If a function
definition contains a "reads { ... }" clause, then every read
_and_ write effect must be listed.
* [drivers] syntax rules, metas, and preludes are inherited
through cloning. Keyword "cloned" becomes unnecessary and
is not accepted anymore.
o [why3ide] allow several files on the command-line
o [ocaml API] incompatible changes in Set/Map/Hashtbl modules
o [ocaml API] examples in the manual extended to API for Why3ml programs
......
# Why version
VERSION=0.81prerelease
VERSION=0.81
......
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