heap_lang/proofmode.v · 27baa1d5920754396d5d00e01da33f83da3849e8 · Jonas Kastberg / iris · GitLab

Find file Blame History Permalink

Let wp_cas_suc generate equality goal if the values are not convertible. · 27baa1d5
Robbert Krebbers authored May 10, 2016
```
This is more consistent with wp_cas_fail.
```
27baa1d5

proofmode.v 6.64 KB