proofmode/intro_patterns.v · a9f8d0f0ba5937059bf0c02e5a9f9969f3638b67 · Marianna Rapoport / iris-coq · GitLab

Find file Blame History Permalink

Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing. · a9f8d0f0
Robbert Krebbers authored Jun 30, 2016
```
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
```
a9f8d0f0