diff --git a/CHANGES.md b/CHANGES.md index 9bd6fd5a8a23cffaa78f19dff7c42536958d8ee9..967f29a185e9a4483998247280c68e1cc29cf658 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -26,6 +26,7 @@ Language * support for type coercions in logic using `meta coercion` * deprecated `theory`; use `module` instead * term on the left of sequence `;` must be of type `unit` :x: + * cloned axioms are now turned into lemmas; use `with axiom foo` to prevent :x: Standard library * machine integers in `mach.int.*` are now range types :x: @@ -34,7 +35,7 @@ Standard library Extraction * improved extraction to OCaml * added partial extraction to C using the memory model of `mach.c` - * added extraction to CakeML (using 'why3 extract -D cakeml ...') + * added extraction to CakeML (using `why3 extract -D cakeml ...`) Transformations * transformations can now have arguments @@ -45,10 +46,10 @@ Drivers * support for `use` in theory drivers IDE - * left toolbar replaced by a context menu + * replaced left toolbar by a contextual menu * source is now editable * premises are no longer implicitly introduced - * command-line interface to call transformations and provers + * added textual interface to call transformations and provers Tools * deprecated `.why` file extension; use `.mlw` instead diff --git a/ROADMAP b/ROADMAP index bd4df617b62b34add6f3902828bcad01cbd7ea0c..6b4a9a843d484f061fc66da0c05d677df1907265 100644 --- a/ROADMAP +++ b/ROADMAP @@ -125,6 +125,7 @@ * generate documentation - update the date in doc/manual.tex (near \whyversion{}) + - check/update the authors in doc/manual.tex - check that macro \todo is commented out in doc/macros.tex - do "make doc" (check that manual in HTML is also generated, doc/html/index.html)