diff options
| author | coq | 2001-04-25 11:01:29 +0000 |
|---|---|---|
| committer | coq | 2001-04-25 11:01:29 +0000 |
| commit | 342ab1e68c5941d1d746c8fafc557934cece2ed0 (patch) | |
| tree | 66b75b2c9d615cd16d65863993bd5d1d5de54ded /doc/Correctness.tex | |
| parent | d84851a91cf7dc1ede95f9af3330770d2d2cf3c8 (diff) | |
Pending ref's corrected
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Correctness.tex')
| -rw-r--r-- | doc/Correctness.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Correctness.tex b/doc/Correctness.tex index 1b24207f64..31d83775cf 100644 --- a/doc/Correctness.tex +++ b/doc/Correctness.tex @@ -681,7 +681,7 @@ $$ \mbox{\texttt{Require ProgramsExtraction.}} $$ This extraction facility extends the extraction of functional programs -(see chapter~\ref{CamlHaskellExtraction}), on which it is based. +(see chapter~\ref{Extraction}), on which it is based. Indeed, the extraction of functional terms (\Coq\ objects) is first performed by the module \texttt{Extraction}, and the extraction of imperative programs comes after. @@ -696,7 +696,7 @@ That list may contain functional and imperative objects, and does not need to be exhaustive. Of course, you can use the extraction facilities described in -chapter~\ref{CamlHaskellExtraction}, namely the \texttt{ML Import}, +chapter~\ref{Extraction}, namely the \texttt{ML Import}, \texttt{Link} and \texttt{Extract} commands. |