The Coq mailing list

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

> Since I installed version 6.3.1, I get all lot of messages
> "Warning: Failed to extract".
> What does it mean and how to make it disappear?

  It means the extraction algorithm has not been successful in finding
a computational content to the involved definition (typically because
the definition involved objets at the Type level). This has no effect
on the logical validity of your definition. You cannot make it
disappear without recompiling (remove the warning in file
src/typing/mach.ml).
                                                  Hugo