From c401fc96c3271746448600ca097876bd139b10e9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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 +-
 test-suite/bugs/closed/5641.v | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5641.v

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index eee227370e..3e516cae04 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
diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v
new file mode 100644
index 0000000000..9f3246f33d
--- /dev/null
+++ b/test-suite/bugs/closed/5641.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j}.
+Proof.
+abstract (exact ltac:(abstract (exact A))).
+Defined.
-- 
cgit v1.2.3