diff options
| -rwxr-xr-x | doc/Extraction.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/Extraction.tex b/doc/Extraction.tex index c315cdf78d..a68969c38a 100755 --- a/doc/Extraction.tex +++ b/doc/Extraction.tex @@ -597,11 +597,11 @@ This will extract all Standard Library files and compile them. It is done via many {\tt Extraction Module}, with some customization (see subdirectory {\tt custom}). -The result of this extraction of the Standard Library can be browsed -at URL -\begin{flushleft} -\url{http://www.lri.fr/~letouzey/extraction}. -\end{flushleft} +%The result of this extraction of the Standard Library can be browsed +%at URL +%\begin{flushleft} +%\url{http://www.lri.fr/~letouzey/extraction}. +%\end{flushleft} %Reals theory is normally not extracted, since it is an axiomatic %development. We propose nonetheless a dummy realization of those |