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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 156c9a2772..bdd9ed81cf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1651,7 +1651,7 @@ let betazetaevar_applist sigma n c l = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar ev, _ -> (match safe_evar_value sigma ev with | Some body -> stacklam n env body stack |