Merge PR #9450: Fix #9432: canonical structure and coercion accept universe binders.

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9432.v b/test-suite/bugs/closed/bug_9432.v
new file mode 100644
index 0000000000..c85f8129ce
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9432.v
@@ -0,0 +1,12 @@
+
+Record foo := { f : Type }.
+
+Fail Canonical Structure xx@{} := {| f := Type |}.
+
+Canonical Structure xx@{i} := {| f := Type@{i} |}.
+
+Fail Coercion cc@{} := fun x : Type => Build_foo x.
+
+Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x.
+
+Coercion cc1@{i} := (cc@{i}).