• Robbert Krebbers's avatar
    Use the sink modality in the proof mode. · f0e57c42
    Robbert Krebbers authored
    Whenever we iSpecialize something whose conclusion is persistent, we now have
    to prove all the premises under the sink modality. This is strictly more powerful,
    as we now have to use just some of the hypotheses to prove the premises, instead of
class_instances.v 48.9 KB