Skip to content
  • Robbert Krebbers's avatar
    Solve Import cofe_solver situation. · cf952456
    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