• Robbert Krebbers's avatar
    Make namespace type classes opaque. · be766197
    Robbert Krebbers authored
    This way we ensure that Coq gives an error message when one accidentially
    writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
    lists.
    be766197