From 6adc6e9484fde99ae943b31989f1454b6d079aaa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Sep 2019 09:17:29 +0200
Subject: Adding documentation for the move of sections data to kernel.

---
 dev/doc/critical-bugs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index d00c8cb11a..78d7061259 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -129,6 +129,18 @@ Universes
   GH issue number: #9294
   risk: moderate risk to be activated by chance
 
+  component: universe polymorphism, asynchronous proofs
+  summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
+  introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
+  impacted released: V8.5-V8.10
+  impacted development branches: none
+  impacted coqchk versions: immune
+  fixed in: PR#10664
+  found by: Pédrot
+  exploit: no test
+  GH issue number: none
+  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
 Primitive projections
 
   component: primitive projections, guard condition
-- 
cgit v1.2.3