
version 1.32
============
  o output for Coq version 8 with --coq-v8
    (--coq is now equivalent to --coq-v7, and is still the default output)
  o Mizar output (with option --mizar)
    Mizar article in lib/mizar/why.miz (installed by "make install")

version 1.3, September 17th, 2003
================================= 
  o new tool why2html to convert Why input files to HTML
  o Simplify output (with option --simplify)
  o fixed bug with WP of constants false/true (simplification added)
  o better automatic annotation of tests (in particular || and && are given
    postconditions whenever possible)

version 1.22, June 21th, 2003
=============================
  o fixed lost of annotation in C function calls
  o C: /*W external/parameter ...*/ correctly added to C environment
  o Coq: added Hints Unfold Zwf
  o (almost) conservative change in renaming strategy; a reference x1 is now
    renamed into x1 x1_0 x1_1 etc. instead of x1 x2 x3 etc.

version 1.2, May 12th, 2003
===========================
  o true used as default postcondition for exceptions instead of false
    (necessary for a correct translation of C programs)
  o C: fixed bug in translation from ints to booleans
  o better names given to local references in proof obligations
  o improved automatic proof (both completeness and performance)

version 1.10, April 4th, 2003
==============================
  o C: added label statement and alternate syntax /*@ label id */ 
  o fixed bug in ocaml code generation

version 1.08, March 28th, 2003
==============================
  o C: local variables can be uninitialized
  o examples: C programs for exact string matching (in string-matching)
  o fixed bug in WP (not collecting some intermediate assertions)
  o C: added statement /*@ assert p */
  o new construct "absurd" to denote unreachable code

version 1.07, March 25th, 2003
==============================
  o arbitrary side-effects now allowed in tests (if / while)
  o label "init" suppressed; new syntax label:expression to insert labels
  o syntax: logic may introduce several identifiers in a single declaration
  o linear proof search restricted to WP obligations
  o PVS: change in array type (warray) to get better TCCs
  o fixed ocaml output (array_length)

version 1.04, March 5th, 2003
=============================
  o C: logic declarations with syntax /*W ... */
  o improved automatic proof (thus less obligations)
  o validation in a separate file f_valid.v

version 1.02, February 7th, 2003
================================
  o PVS: fixed integer division and modulo, fixed output
  o haRVey: no more restriction to first-order obligations
  o Coq: the validation is now given a type
  o distinction between preconditions and obligations

version 1.0, January 31st, 2003
================================
  o syntax: pre- and postconditions brackets now come by pairs (but,
    inside, the predicates may be omitted)
  o fixed WP bug in a sequence of calls with before-after annotations
  o no more "pvs" declaration (the user can now edit the _why.pvs file)
  o fixed bug in type-checking of recursive functions with exceptions
  o fixed bug in loop tests automatic annotation; 
    now a warning when a loop test cannot be given a postcondition
  o fixed bug in interpretation of @init 
  o doc: C programs, Coq and PVS libraries documented
  o logic: if-then-else construct on terms
  o PVS: arrays defined in Why prelude and fixed pretty-print; installation

version 0.92, January 13th, 2003
================================
  o C: fixed bug in array/reference passing
  o fixed check for exceptions in external declarations
  o HOL Light output (with option --hol-light)
  o fixed compatibility with Coq 7.3
  o C: recursive functions, arrays, pointers

version 0.8, December 6th, 2002
===============================
  o haRVey output (option --harvey; see http://www.loria.fr/~ranise/haRVey/)
  o C input (incomplete: no arrays, no pointers, no recursive functions)
  o Coq: helper tactics (AccessSame, AccessOther, ...)
  o fixed bug in application typing
  o major change:
    arrays do not have a dependent type anymore; array_length introduced
  o Emacs mode for editing Why ML source (in lib/emacs)
  o automatic discharge of ...|-(well_founded (Zwf 0))
    and of ...,v=t,...,I and (Zwf 0 t' t),...|-(Zwf 0 t' v)
  o fixed bug in local recursive functions

version 0.72, November 12th, 2002
=================================
  o caml code generation with option --ocaml (beta test)
    (customized with --ocaml-annot, --ocaml-ext, --output)
  o quantifier "exists" added to the logic syntax
  o manual: added lexical conventions
  o examples: added maximum sort (by Sylvain Boulm)
  o new feature: exceptions (beta test)

version 0.71, October 15th, 2002 (bug fix release)
================================
  o better WP for the if-then-else (when the test is annotated)
  o reference masking now forbidden
  o fixed bug in automatic annotations => some postconditions names may change
  o fixed Coq 7.3 compatibility module

version 0.7, October 2nd, 2002
==============================
  o Why library compatible with Coq 7.3 (released version) and with Coq
    development version (determined at configuration)
  o code ported to ocaml 3.06  
  o examples: quicksort (2 versions) 
  o more obligations automatically discharged 
    (True  /  A and B |- A  /  A,B |- A and B)
  o Coq: fixed associativity in pretty-print for /\ and \/ (right)
    right associativity adopted in Why
  o fixed typing and Coq output for primitive float_of_int

version 0.6, July 19th, 2002
============================
  o examples: find
  o doc: predefined functions and predicates
  o floats: predefined functions and predicates, Coq pretty-print
  o fixed bug: x@ reference in a loop post-condition incorrectly translated
  o the variant relation is now necessarily an identifier
  o terms and predicates are now typed; new declaration "logic"
    (terms and predicates syntax are mixed; fixes a parsing bug)

version 0.5,  July 2nd, 2002
============================
  o first (beta) release
