Commit 1eedd141 authored by MARCHE Claude's avatar MARCHE Claude

minor changes in changes and manual before the release

parent cc8215e3
...@@ -45,6 +45,7 @@ Drivers ...@@ -45,6 +45,7 @@ Drivers
* support for `use` in theory drivers * support for `use` in theory drivers
IDE IDE
* left toolbar replaced by a context menu
* source is now editable * source is now editable
* premises are no longer implicitly introduced * premises are no longer implicitly introduced
* command-line interface to call transformations and provers * command-line interface to call transformations and provers
......
VERSION=0.90+git VERSION=1.00+git
...@@ -118,7 +118,7 @@ ...@@ -118,7 +118,7 @@
%BEGIN LATEX %BEGIN LATEX
\begin{LARGE} \begin{LARGE}
%END LATEX %END LATEX
Version \whyversion{}, January 2018 Version \whyversion{}, June 2018
%BEGIN LATEX %BEGIN LATEX
\end{LARGE} \end{LARGE}
%END LATEX %END LATEX
...@@ -151,7 +151,7 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120 ...@@ -151,7 +151,7 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
\bigskip \bigskip
%END LATEX %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{\urlutcat}{\url}{http://frama-c.com/u3cat/}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/} \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. ...@@ -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 is available there, in source format, together with this documentation
and several examples. 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 \why is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}. 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: ...@@ -220,9 +223,11 @@ Report any bug to the \why Bug Tracking System:
We gratefully thank the people who contributed to \why, directly or We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, L\'eon Gondelman, Johannes Kanig, St\'ephane Clochard, Simon Cruanes, Sylvain Dailler, Cl\'ement Fumex, L\'eon
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate, Gondelman, David Hauzar, Daisuke Ishii, Johannes Kanig, St\'ephane
Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek. 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 \cleardoublepage
......
...@@ -4,6 +4,10 @@ ...@@ -4,6 +4,10 @@
In this chapter, we describe the syntax and semantics of \whyml. 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} \section{Lexical Conventions}
\label{sec:lexer} \label{sec:lexer}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment