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.
---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3