proofmode/tactics.v · a9f8d0f0ba5937059bf0c02e5a9f9969f3638b67 · Michael Sammler / iris-coq · GitLab

Snippets Groups Projects

Forked from Iris / Iris

3514 commits behind the upstream repository.

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

History
Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.
Robbert Krebbers authored 8 years ago
```
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
```