Fourier, Reals,...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8201 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 13 deletions

diff --git a/doc/Changes.tex b/doc/Changes.tex
index 2ec6ed3189..e4af1b996a 100755
--- a/doc/Changes.tex
+++ b/doc/Changes.tex
@@ -307,13 +307,15 @@ details, see the Reference Manual.
 
    \paragraph{{\tt Fourier}} written by LoÏc Pottier solves linear inequations.
 
-   \paragraph{Others tactics and developments} has been included in the Reals
-library: {\tt DiscrR} prove that a real integer constante c1 is non equal to
-another real integer constante c2; {\tt SplitAbsolu} allows us to split 
-Rabsolu; {\tt SplitRmult} allows us to split Rabsolu a product non equal to 
-zero and give the corresponding subgoals with each term non equal to zero.
-All this tactics has been written with the tactic language $\ltac$.\\
-A development on Cauchy series, power series,... has been added.\\
+   \paragraph{Other tactics and developments} has been included in the real
+numbers library: {\tt DiscrR} proves that a real integer constant c1 is non 
+equal to another real integer constant c2; {\tt SplitAbsolu} allows us to 
+unfold {\tt Rabsolu} contants and split corresponding conjonctions; 
+{\tt SplitRmult} allows us to split a condition that a product is non equal to 
+zero into subgoals corresponding to the condition on each subterm of the 
+product. All these tactics have been written with the tactic language 
+$\ltac$.\\ 
+A development on Cauchy series, power series,... has been also added.\\
 For more details, see the Reference Manual.
 
 \subsection{Changes in pre-existing tactics}
@@ -525,9 +527,9 @@ located in the source file.
 \section{Extraction}\label{Extraction}
 Extraction code has been completely rewritten since version V6.3. 
 This work is still not finished, but most parts of it are already
-usable. It was successfully tested on the \coq{} theories.
+usable. It was successfully tested on the {\Coq} theories.
 
-The new mechanism is able to extract programs from any \coq{} term
+The new mechanism is able to extract programs from any {\Coq} term
 (including terms at the Type level). 
 
 However, the resulting ML term is not guaranteed to be typable in ML
@@ -540,7 +542,7 @@ A new mechanism to extract Ocaml modules from Coq files has been
 added. 
 
 The \verb!ML import! command is not available anymore, use the command
-\verb!Extract Constant! to realize a \coq{} axiom by an ML program.
+\verb!Extract Constant! to realize a {\Coq} axiom by an ML program.
 
 The syntax of commands is described in the Reference Manual.
 
@@ -574,11 +576,13 @@ documentation tool (see the ``doc'' directory in {\Coq} source).
   \item Default parsers in {\tt Grammar} and {\tt Syntax} are
   different (see section \ref{GrammarSyntax}).
   
-  \item Definition of {\tt D\_in} (Reals/Rderiv.v) is now with Rdiv (Rmult and 
-        Rinv before).
+  \item Definition of {\tt D\_in} (Rderiv.v) is now with Rdiv and not 
+        with Rmult and Rinv as before.
+
+  \item {\tt Extraction} is currently not available in {\Coq} V7.
 
   \item Pattern aliases of dependent type in \verb=Cases=
-  expressions are currently not supported.
+        expressions are currently not supported.
 
   \end{itemize}