paragraphe obsolete sur l'extraction

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

1 files changed, 0 insertions, 12 deletions

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 3dfe40617c..bf8414ca1e 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -103,18 +103,6 @@ have {\sf Type :Type}.
 We shall make precise in the typing rules the constraints between the
 indexes.
 
-\medskip
-\Rem
-The extraction mechanism is not compatible with this universe
-hierarchy. It is supposed to work only on terms which are explicitly
-typed in the Calculus of Constructions without universes and with
-Inductive Definitions at the Set level and only a small elimination.
-In other cases, extraction may generate a dummy answer and sometimes
-failed. To avoid failure when developing proofs, an error while
-extracting the computational contents of a proof will not stop the
-proof but only give a warning.
-
-
 \subsection{Constants}
 Besides the sorts, the language also contains constants denoting
 objects in the environment. These constants may denote previously