From 1e92ed4d129aea5ea4e9300a24e1135cc186c341 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:30:07 +0200
Subject: Fix Canonical with universe polymorphism and primitive projection

Perhaps we should thread an evar map with the Var universes added
through to cs_pattern_of_constr but that would be significantly more invasive.

Fix #12528
---
 test-suite/bugs/closed/bug_12528.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12528.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_12528.v b/test-suite/bugs/closed/bug_12528.v
new file mode 100644
index 0000000000..4ab05ac9b8
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12528.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Set Universe Polymorphism.
+Record ptd := Ptd { t : Type ; p : t }.
+Definition type := Ptd Type (unit:Type).
+Definition type' := Ptd Type (p type).
+Canonical type'.
-- 
cgit v1.2.3