-
Robbert Krebbers authored
Requires should always be at the top of a file, Imports can be inside of submodules. It is strange that a Require in a submodule is allowed and then triggers an error when using the whole module. This may be a Coq bug.
cf952456