Skip to content
  • Robbert Krebbers's avatar
    Strengthen `tac_specialize_assert` to put the result in the intuitionistic context. · 1fcbf679
    Robbert Krebbers authored
    The result of `iSpecialize ("H" with "[H1 .. Hn]")` was always put in the
    spatial context. This commit strenghtens this tactic by putting the result
    in the intuitionistic context if the following conditions hold:
    
    1. The hypothesis `H` is persistent.
    2. All the hypotheses `H1 .. Hn` are intuitionistic (or similarly, in case
       `[-H1 .. Hn]` is used, if all remaining hypotheses are intuitionistic).
    3. If the pattern `[> ..]` for adding a modality is not used.
    1fcbf679