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

(when defining a new constant)

2 files changed, 14 insertions, 4 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..c074f1cfc1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9432.v
@@ -0,0 +1,10 @@
+
+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.
+
+Coercion cc@{i} := fun x : Type@{i} => Build_foo x.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 0664e18130..e7d81b8bb0 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -697,14 +697,14 @@ GRAMMAR EXTEND Gram
           { VernacCanonical CAst.(make ~loc @@ AN qid) }
       | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
           { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
-      | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
+      | IDENT "Canonical"; IDENT "Structure"; qid = global; u = OPT univ_decl; d = def_body ->
           { let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) }
+          VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) }
 
       (* Coercions *)
-      | IDENT "Coercion"; qid = global; d = def_body ->
+      | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body ->
           { let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) }
+          VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) }
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
            { VernacIdentityCoercion (f, s, t) }