prelude/tactics.v · 77a15fea647d8d775556879ab6a8992529840aa7 · Iris / Iris · 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