From 1eedd1418dfe8b4cde09d5f5d2da613fc321da52 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 22 Jun 2018 16:06:34 +0200
Subject: [PATCH] minor changes in changes and manual before the release
---
CHANGES.md | 1 +
Version | 2 +-
doc/manual.tex | 15 ++++++++++-----
doc/syntaxref.tex | 4 ++++
4 files changed, 16 insertions(+), 6 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 172edae3c..9bd6fd5a8 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 5caad31fc..a9450123e 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 1027efc71..0ca3d1316 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 0bff324da..a861a5523 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}
--
GitLab