From c401fc96c3271746448600ca097876bd139b10e9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 11 Jul 2017 15:26:44 +0200
Subject: Fix nonsensical universe abstraction in the kernel.

The function turning a side-effect declaration into the corresponding
entry was crazily wrong, as it used a named universe context quantifying
over DeBruijn universe indices. Declaring such entries resulted
in random anomalies.

This fixes bug #5641.
---
 kernel/term_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index eee227370..3e516cae0 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -469,7 +469,7 @@ let constant_entry_of_side_effect cb u =
     match cb.const_universes with
     | Monomorphic_const ctx -> false, ctx
     | Polymorphic_const auctx -> 
-      true, Univ.instantiate_univ_context auctx
+      true, Univ.AUContext.repr auctx
   in
   let pt =
     match cb.const_body, u with
-- 
cgit v1.2.3