diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-21 00:23:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 12:10:07 +0100 |
| commit | e583a79b5a0298fd08f34305cc876d5117913e95 (patch) | |
| tree | b8932df86a8cfb987e5c383ead66ff3afe123e8e /kernel/reduction.ml | |
| 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/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 892557ac6..939eeef5d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -136,7 +136,7 @@ let betazeta_appvect n c v = 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 | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) |