diff --git a/CHANGES.md b/CHANGES.md
index d3cde36af6faf4c609d0a83cbdbe37d2b1df9b93..d4b65724db0ca135c702bfa62c083c579e8a02ee 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,28 +1,31 @@
 :x: marks a potential source of incompatibility
 
+Version 1.0.0, June 25, 2018
+----------------------------
+
 Core
   * improved support of counter-examples
+  * attribute `[@vc:sp]` on an expression switches from traditional WP
+    to Flanagan-Saxe-like VC generation
+  * type invariants now produce logical axioms;
+    a type with an invariant must be proved to be inhabited :x:
+  * logical symbols can no longer be used in non-ghost code;
+    in particular, there is no polymorphic equality in programs any more,
+    so equality functions must be declared/defined on a per-type basis
+    (already done for type `int` in the standard library) :x:
 
 Language
   * numerous changes to syntax, see documentation appendix :x:
   * `let function`, `let predicate`, `val function`, and `val predicate`
      introduce symbols in both logic and programs
-  * logical symbols can no longer be used in non-ghost code;
-    in particular, there is no polymorphic equality in programs any more,
-    so equality functions must be declared/defined on a per-type basis
-    (already done for type `int` in the standard library) :x:
   * added overloading of program symbols
   * new contract clause `alias { <term> with <term>, ... }` :x:
   * support for parallel assignment `<term>,... <- <term>,...`
-  * type invariants now produce logical axioms;
-    a type with an invariant must be proved to be inhabited :x:
   * support for local exceptions using `exception ... in ...`
   * added `break`, `continue`, and `return` statements
   * support for `exception` branches in `match` constructs
   * support for `for` loops on range types
     (including machine integers from the standard library)
-  * attribute `[@vc:sp]` on an expression switches from traditional WP
-    to Flanagan-Saxe-like VC generation
   * support for type coercions in logic using `meta coercion`
   * keyword `theory` is deprecated; use `module` instead
   * term on the left of sequence `;` must be of type `unit` :x:
diff --git a/ROADMAP b/ROADMAP
index 6b4a9a843d484f061fc66da0c05d677df1907265..98eba54cb1778848fa22a28ee86bd2b4a7438384 100644
--- a/ROADMAP
+++ b/ROADMAP
@@ -112,7 +112,6 @@
 ============ Making a release ============
 
 * check the BTS
-* do "make update-coq" and "make", fix Coq realizations if needed
 * check that nightly bench is OK
 * check that "make xml-validate-local" is OK
   (see below : copy the dtd on the web)
diff --git a/Version b/Version
index a9450123ef5b96d493f0fffb266e2a96e61ac39a..624badec2f6079e314a31c2ddbb1843a69af66cc 100644
--- a/Version
+++ b/Version
@@ -1 +1 @@
-VERSION=1.00+git
+VERSION=1.0.0