diff options
| author | Tej Chajed | 2020-02-15 11:39:56 -0500 |
|---|---|---|
| committer | Tej Chajed | 2020-02-28 07:39:41 -0500 |
| commit | 721b6704a0fbee1be627c67e0a883fa40a81deb6 (patch) | |
| tree | 3afb107af1cca2a49cc7ff67b8ed76882035be2c /dev/ci/ci-iris-lambda-rust.sh | |
| parent | d122f7d5ffd5d3b26153a0ad7b74a669b8dd1c9d (diff) | |
[stm] Use Default Proof Using only with Proof
Fixes #11608.
This means -vos doesn't skip proofs for definitions that end with Qed
but don't include Proof and rely on a Set Default Proof Using. However,
this fixes the bug where this pattern would instead hang, due to #11564.
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
0 files changed, 0 insertions, 0 deletions