diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 17:04:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 0eadf776ba78dcfdcab842f38f5de871ed337376 (patch) | |
| tree | d45d4b138a56b303ee40d0013911be115c538268 /plugins/funind | |
| parent | 7a2e41abd8559d0bd4683e513dcb0b83987a9128 (diff) | |
[proof] [stm] Force `opaque` in `close_future_proof`
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions