diff options
| author | Pierre-Marie Pédrot | 2020-11-09 21:36:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-12 10:57:05 +0100 |
| commit | 0ca664107a1e60dfa47aa7536e30a348456efe44 (patch) | |
| tree | 57f9c57e7544ac4aad2c7d5f58c17d0fa26b1403 /dev | |
| parent | 9dfc627ccac11b46bc11bcc11e9609b952d35fdd (diff) | |
Fix #13330: Kernel messes with polymorphic side-effects.
Polymorphic side-effects generated in monomorphic mode would be counted towards
trusted subcomponents. This would allow to make ill-typed terms pass as
legitimate by mimicking the shape of the inlining of monomorphic side-effects in
such a proof.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions