The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

  Dear Mark-Oliver,

> 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
>
> ...
>
> 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. 

  Yes, the warning means Coq has not been able to extract a
computation meaning of the proof. This occurs typically when handling
objects at the Type level.

  It does not invalidate the correctness of the proof. Just that a
program won't be extracted from the proof.

  Best wishes,

                                                  Hugo