algebra/upred.v · 2ee38008bc235c1886caa38c98c0434910847cd1 · Joshua Yanovski / iris-coq · GitLab

Find file Blame History Permalink

write a tactic that can solve Proper goals, and use it in a few places · 77a15fea
Ralf Jung authored Feb 25, 2016
```
This replaces f_equiv and solve_proper with our own, hopefully better, versions
```
77a15fea