diff options
| -rwxr-xr-x | doc/Changes.tex | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/Changes.tex b/doc/Changes.tex index bf2742466..7b10f4f82 100755 --- a/doc/Changes.tex +++ b/doc/Changes.tex @@ -12,6 +12,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7} + %This document describes the main differences between {\Coq} V6.3.1 and %V7. This new version of {\Coq} is characterized by fixed bugs, and %improvement of implicit arguments synthesis and speed in tactic @@ -335,10 +336,10 @@ can be visited at the following URL:\\ {\sf http://logical.inria.fr/\~{}delahaye/} -\paragraph{Tactic debuger} +\paragraph{Tactic debugger} \paragraph{{\tt Debug $($ On $|$ Off $)$}} turns on/off the tactic - debuger for $\ltac$. + debugger for $\ltac$. This is still very experimental and no documentation is provided yet. @@ -511,6 +512,7 @@ Print exists. Implicits exists [1]. Print exists. \end{coq_example} + \subsection{Syntax standardisation} The commands on the left are now equivalent to (old) commands on |