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.
---
 dev/doc/critical-bugs | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 78d7061259..6d90ced12d 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -250,6 +250,17 @@ Conversion machines
   exploit: test-suite/bugs/closed/bug_9684.v
   GH issue number: #9684
 
+  component: lazy machine
+  summary: incorrect De Bruijn handling when inferring the relevance mark for a lambda
+  introduced: 2019-03-15, 23f84f37c674a07e925925b7e0d50d7ee8414093 and 71b9ad8526155020c8451dd326a52e391a9a8585, SkySkimmer
+  impacted released versions: 8.10.0
+  impacted coqchk versions: 8.10.0
+  found by: ppedrot investigating unexpected conversion failures with SProp
+  exploit: test-suite/bugs/closed/bug_10904.v
+  GH issue number: #10904
+  risk: none without using -allow-sprop (off by default in 8.10.0),
+        otherwise could be exploited by mistake
+
 Conflicts with axioms in library
 
   component: library of real numbers
-- 
cgit v1.2.3