heap_lang/lib/barrier/proof.v · 5c1f62d73ed4ef91452f86e885a58018d8968dff · Ike Mulder / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago
99fd8e5b
Make iPure and iPersistent internal to reduce the number of tactics. · 99fd8e5b
Robbert Krebbers authored 8 years ago
```
These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"
```
99fd8e5b

History
Make iPure and iPersistent internal to reduce the number of tactics.
Robbert Krebbers authored 8 years ago
```
These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"
```