The Coq mailing list

[Vincent Cremet <vincent.cremet AT epfl.ch>]

Hi,

The module system of Coq makes it possible to declare hypotheses in a
module. I was wondering if there exists a means for the user to know
what hypotheses have been made in the modules he has decided to
use. This is of particular interest if we are using a library of
several million lines and we don't want to check manually that there
is no inconsistent axiom in one of its modules.

I apologize in advance if I missed something in the documentation.

Sincerely.

Vincent Cremet.
---------------------------------
Laboratory of Programming Methods
EPFL- Lausanne - Switzerland