From 342ab1e68c5941d1d746c8fafc557934cece2ed0 Mon Sep 17 00:00:00 2001
From: coq
Date: Wed, 25 Apr 2001 11:01:29 +0000
Subject: Pending ref's corrected

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8207 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Correctness.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/Correctness.tex')

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.
 
 
-- 
cgit v1.2.3