The Coq mailing list

[Mark-Oliver Stehr <stehr AT informatik.uni-hamburg.de>]

I just switched to the new 6.3.1 version of
COQ and it seems that the following warning
ocurrs more often than in previous versions:

Warning: Failed to extract

The warning appears after finishing a proof
with Qed. Nevertheless the proof object
seems to be correctly generated under the name of the
theorem.

So the question is: What does this warning
mean precisely, in particular, can I be sure
that the proof is valid ?

I suspect that the warning has to do something
with program extraction, a feature that I am 
currently not using. 

Thanks in advance,
Mark-Oliver

-- 
Mark-Oliver Stehr
Universit"at Hamburg, Fachbereich Informatik
Arbeitsbereich Theoretische Grundlagen der Informatik
Vogt-K"olln-Str. 30, D-22527 Hamburg
Tel. +49-40-42883-2245  **  (Fax -2246)
e-mail: 
stehr AT informatik.uni-hamburg.de
http://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr.html