diff --git a/CHANGES.md b/CHANGES.md
index 172edae3cfa7dc849eb189fc7276e5ac0bd0ad4b..9bd6fd5a8a23cffaa78f19dff7c42536958d8ee9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -45,6 +45,7 @@ Drivers
   * support for `use` in theory drivers
 
 IDE
+  * left toolbar replaced by a context menu
   * source is now editable
   * premises are no longer implicitly introduced
   * command-line interface to call transformations and provers
diff --git a/Version b/Version
index 5caad31fc7690ad6dfbce157e1e27e16f01fc15e..a9450123ef5b96d493f0fffb266e2a96e61ac39a 100644
--- a/Version
+++ b/Version
@@ -1 +1 @@
-VERSION=0.90+git
+VERSION=1.00+git
diff --git a/doc/manual.tex b/doc/manual.tex
index 1027efc71e682ab79122accfaa53579b3dccf227..0ca3d1316faf2627433f24fab23cb785e4c7cbc0 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -118,7 +118,7 @@
 %BEGIN LATEX
 \begin{LARGE}
 %END LATEX
-  Version \whyversion{}, January 2018
+  Version \whyversion{}, June 2018
 %BEGIN LATEX
 \end{LARGE}
 %END LATEX
@@ -151,7 +151,7 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
 \bigskip
 %END LATEX
 
-\textcopyright 2010--2016 University Paris-Sud, CNRS, Inria
+\textcopyright 2010--2018 University Paris-Sud, CNRS, Inria
 
 \urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
 \urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
@@ -200,6 +200,9 @@ formalizations or to add support for a new external prover if wanted.
 is available there, in source format, together with this documentation
 and several examples.
 
+\why is also distributed under the form of an OPAM package and a
+Debian package.
+
 \why is distributed as open source and freely available under the
 terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.
 
@@ -220,9 +223,11 @@ Report any bug to the \why Bug Tracking System:
 
 We gratefully thank the people who contributed to \why, directly or
 indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
-Clochard, Simon Cruanes, L\'eon Gondelman, Johannes Kanig, St\'ephane
-Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
-Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
+Clochard, Simon Cruanes, Sylvain Dailler, Cl\'ement Fumex, L\'eon
+Gondelman, David Hauzar, Daisuke Ishii, Johannes Kanig, St\'ephane
+Lescuyer, Mikhail Mandrykin, David Mentr\'e, Sim\~ao Melo de Sousa,
+Benjamin Monate, Kim Nguyen, Thi-Minh-Tuyen Nguyen, M\'ario Pereira,
+Asma Tafat, Piotr Trojanek, Makarius Wenzel.
 
 
 \cleardoublepage
diff --git a/doc/syntaxref.tex b/doc/syntaxref.tex
index 0bff324da5cc31d8bdf05f17dc2b27558d00f29c..a861a55233fc11ca99c6e97288fad847aea5db26 100644
--- a/doc/syntaxref.tex
+++ b/doc/syntaxref.tex
@@ -4,6 +4,10 @@
 
 In this chapter, we describe the syntax and semantics of \whyml.
 
+This chapter is not yet fully updated to the new syntax of \why 1.00, so it not distributed for the moment.
+
+\endinput
+
 \section{Lexical Conventions}
 \label{sec:lexer}