diff options
| author | Hugo Herbelin | 2015-11-21 00:23:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-22 12:10:07 +0100 |
| commit | e583a79b5a0298fd08f34305cc876d5117913e95 (patch) | |
| tree | b8932df86a8cfb987e5c383ead66ff3afe123e8e /kernel/nativelambda.mli | |
| parent | 8d93301045c45ec48c85ecae2dfb3609e5e4695f (diff) | |
Fixing kernel bug in typing match with let-ins in the arity.
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions