theories/proofmode/tactics.v · e0789039ed0dcb01b6249fec2d5a36f66e5de21c · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago
e0789039
Make it optional that iPoseProofCore performs TC inference lazily. · e0789039
Robbert Krebbers authored 8 years ago
```
For iApply and iRewrite we want that, but for iDestruct and iMod we do not.

This fixes issue #52.
```
e0789039

History
Make it optional that iPoseProofCore performs TC inference lazily.
Robbert Krebbers authored 8 years ago
```
For iApply and iRewrite we want that, but for iDestruct and iMod we do not.

This fixes issue #52.
```