From e398b8b5dadb0cd75cd6cfb86525ccb039d75d49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 28 May 2018 01:00:23 +0200
Subject: Fix #7615: Functor inlining drops universe substitution.

We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 787c9ba12..ce8e313b9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,7 @@ Changes from 8.8.0 to 8.8.1
 Kernel
 
 - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with inlining of polymorphic constants (#7615).
 
 Notations
 
-- 
cgit v1.2.3