diff options
| author | Emilio Jesus Gallego Arias | 2019-06-22 02:37:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-09 12:42:03 +0200 |
| commit | 515e7039857d85f7c6eec9272e0ca3b45162d978 (patch) | |
| tree | 6723753bf51c949c0729e8fcec94451df0a2e099 /kernel/nativecode.mli | |
| parent | 7f366a7c7cd154c6a1dd191ff7f453e63b39a948 (diff) | |
[proof] Remove sign parameter to open_lemma.
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions