From d2e02d2b459a93067064dcc196a2cb35769dc036 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 22 Jun 2018 17:22:56 +0200
Subject: [PATCH] Update changes and release process.
---
CHANGES.md | 7 ++++---
ROADMAP | 1 +
2 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 9bd6fd5a8..967f29a18 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 bd4df617b..6b4a9a843 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)
--
GitLab