From b5aa02f5a0a3b6f6455ca885544e6d61379dd87f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 11 Apr 2002 14:07:32 +0000
Subject: paragraphe obsolete sur l'extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8275 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-cic.tex | 12 ------------
 1 file changed, 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
-- 
cgit v1.2.3