diff options
Diffstat (limited to 'doc/refman/Extraction.tex')
| -rw-r--r-- | doc/refman/Extraction.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index ba07182a6..8271c7c32 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -620,7 +620,7 @@ quite efficient for Caml code. As a test, we propose an automatic extraction of the Standard Library of \Coq. In particular, we will find back the two previous examples, {\tt Euclid} and {\tt Heapsort}. -Go to directory {\tt contrib/extraction/test} of the sources of \Coq, +Go to directory {\tt plugins/extraction/test} of the sources of \Coq, and run commands: \begin{verbatim} make tree; make @@ -653,7 +653,7 @@ also work, just adapt the {\tt Makefile.haskell}. In particular {\tt Some pathological examples of extraction are grouped in the file \begin{verbatim} -contrib/extraction/test_extraction.v +plugins/extraction/test_extraction.v \end{verbatim} of the sources of \Coq. |