From 5c5790d587ad425a882ea8bcdcf28d5ac046aaa3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Oct 2019 21:33:31 +0200
Subject: Fix a De Bruijn bug in the computation of term relevance in the
 kernel.

Opening up a lambda should always lift the substitution attached to it.
---
 kernel/retypeops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index a51b762f95..f398e6a5da 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -71,6 +71,7 @@ let rec relevance_of_fterm env extra lft f =
       | FLambda (len, tys, bdy, e) ->
         let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
         let lft = Esubst.el_liftn len lft in
+        let e = Esubst.subs_liftn len e in
         relevance_of_term_extra env extra lft e bdy
       | FLetIn (x, _, _, bdy, e) ->
         relevance_of_term_extra env (x.binder_relevance :: extra)
-- 
cgit v1.2.3