Commit d8bfd964 authored by MARCHE Claude's avatar MARCHE Claude

update doc: no more option -get-ce

parent 27049598
......@@ -231,8 +231,8 @@ The provers can give the following output:
\label{sec:proveoptions}
\begin{description}
\item[\texttt{-{}-get-ce}] activates the generation of a potential
counter-example when a proof does not succeed (experimental).
%\item[\texttt{-{}-get-ce}] activates the generation of a potential
%counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
\textsl{s} as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
......@@ -242,6 +242,8 @@ counter-example when a proof does not succeed (experimental).
\section{The \texttt{ide} Command}
\label{sec:ideref}
\todo{Claude: mettre a jour}
The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. There are no specific command-line options,
apart from the common options detailed in introduction to this
......@@ -501,8 +503,8 @@ Counter-example.
The counterexample is displayed with the original Why3 code in comments.
Counterexample values for Why3 source code elements at given line are
displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command.
%An alternative way how to display a counterexample is to use the option
%\texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elements that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a
......
......@@ -4,6 +4,7 @@
%BEGIN LATEX
\usepackage{comment}
\usepackage{todonotes}
\newcommand{\ahref}[2]{{#2}}
\excludecomment{htmlonly}
\newenvironment{latexonly}{}{}
......@@ -112,7 +113,7 @@
\vfill
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
%BEGIN LATEX
\begin{LARGE}
......
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