plus de http://www.lri.fr/~letouzey/extraction

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

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index c315cdf78..a68969c38 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