From e583a79b5a0298fd08f34305cc876d5117913e95 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:23:12 +0100
Subject: 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.
---
 kernel/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 892557ac6c..939eeef5d5 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)
 
-- 
cgit v1.2.3