From 44a669e591ee00bcea65b229429dcb5d4d3515ec Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 00:28:15 +0200
Subject: [native compiler] Fix critical bug with primitive projections

Since e1e7888, stuck projections were not computed correctly.

Fixes #9684
---
 dev/doc/critical-bugs | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index c0a5b9095c..f532e1b68f 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -207,6 +207,15 @@ Conversion machines
   GH issue number: ?
   risk: 
 
+  component: primitive projections, native_compute
+  summary: stuck primitive projections computed incorrectly by native_compute
+  introduced: 1 Jun 2018, e1e7888a, ppedrot
+  impacted released versions: 8.9.0
+  impacted coqchk versions: none
+  found by: maximedenes exploiting bug #9684
+  exploit: test-suite/bugs/closed/bug_9684.v
+  GH issue number: #9684
+
 Conflicts with axioms in library
 
   component: library of real numbers
-- 
cgit v1.2.3