From cab5e98780deb1bb65dbeef5d558376f8e34bccc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Dec 2017 11:24:59 +0100
Subject: Fix #5368: Canonical structure unification fails.

Universe instances were lost during constructions of the canonical instance.
---
 test-suite/bugs/closed/5368.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/5368.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5368.v b/test-suite/bugs/closed/5368.v
new file mode 100644
index 0000000000..410fe1707d
--- /dev/null
+++ b/test-suite/bugs/closed/5368.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Record cantype := {T:Type; op:T -> unit}.
+Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}.
+
+Check (op _ ((fun (_:unit) => Set):_)).
-- 
cgit v1.2.3