Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Project Filelist for Why3

File Release Notes and Changelog

Release Name: 0.85

Release Notes
Mainly a bug-fix release, in particular to fix two soundness bugs
Change Log
  * fix a soundness bug in the detection of aliases when calling a
    WhyML function: some alias could have been forgotten when a type
    variable was substituted with a mutable type

  o use the full path of identifiers when the user introduces namespaces
    (BTS #17181)

  * fix a soundness bug in "compute_in_goal" regarding the handling of
    logical implication.
  o several improvements to "compute_in_goal":
    . left-hand side of rewrite rules can be any symbols, not only
      non-interpreted ones.
    . perform beta-reduction when possible
    . the maximal number of reduction steps can be increased using meta
    . the transformation is documented in details in the manual
  o new transformation "compute_specified":
    less aggressive variant of "compute_in_goal".
    Unfolding of definitions is controlled using meta "rewrite_def".
  o fixed a bug in "eliminate_if" when applied on inductive definitions

  o fixed wrong warning when detecting Isabelle2014