From 013191d01d4d96bfbedfaea6513ab61aede1089f Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 6 Jul 2005 15:47:00 +0000 Subject: 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 --- doc/Extraction.tex | 10 +++++----- 1 file 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 -- cgit v1.2.3