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. --- test-suite/bugs/closed/5641.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/5641.v (limited to 'test-suite/bugs/closed/5641.v') diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v new file mode 100644 index 000000000..9f3246f33 --- /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