Implementing Modules in the Coq System

The paper describes the implementation of interactive ML-style modules in the recent version 7.4 of Coq proof assistant. Modules (especially higherorder) provide a very convenient tool for parametrized theories which was lacking in Coq for years. Their interactive character extends naturally the interactive environment provided by the proof assistant. The implementation follows the paradigm of recent versions of Coq to separate the correctnesscritical code from the rest of the system, using abstraction barriers