CHANGES 1.57 KB
Newer Older
1

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
2 3 4
version 0.64, Feb 16, 2011
==========================

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
5
  o algebraic types: must be well-founded, non-positive constructors
MARCHE Claude's avatar
MARCHE Claude committed
6
    are forbidden, recursive functions and predicates must
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
7 8
    structurally terminate
  o syntax: /\ renamed into && and \/ into ||
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11
  o accept lowercase names for axioms, lemmas, goals, and cases in
    inductive predicates
  o labels in terms and formulas are not printed by default. 
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
12 13 14 15 16 17 18 19 20 21 22
  o transformation split-goal does not split under disjunction anymore
  o fixed --enable-local
  o why.conf is no more looked for in the current directory; use -C or
    WHY3CONFIG instead
  o why.conf: when changed, a backup up copy is made in why.conf.bak
  o why.conf now contains a magic number; configuration must be
    rebuilt with why3config if the magic number has changed
  o why3config: --autodetect-provers renamed to --detect-provers
                --autodetect-plugins renamed to --detect-plugins
     new option --detect to perform both detections
  o why3config: --conf_file is replaced by -C and --config
MARCHE Claude's avatar
MARCHE Claude committed
23
  o TPTP: encoding by explicit polymorphism is not anymore the
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
24
    default encoding for TPTP provers. It is now forbidden to use this
MARCHE Claude's avatar
MARCHE Claude committed
25
    encoding in presence of finite types.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
26
  o IDE: source file names are stored in database with paths relative
27 28 29
    to the database, so that databases are now easier to move from a
    machine to another (e.g when they are stored in source control
    repositories)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
30
  o better Gappa output: support for sqrt, for negative constants
31 32 33 34 35

version 0.63, Dec 21, 2010
==========================

  o first public release. See release notes in manual