Coq’s Require Import vs Require Export

The difference between Require Import MyModule and Require Export MyModule is well explained in the modules tutorial:

If a required module depends on other modules then the latter’s are automatically required beforehand. However their contents are not automatically visible. If you want a module M required in a module N to be automatically visible when N is required, you should use Require Export M in your module N.

Leave a Reply

Your email address will not be published. Required fields are marked *