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

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

4 files changed, 28 insertions, 34 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 437b8e557e..933f07674a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1924,9 +1924,10 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: Canonical Structure @qualid
+.. cmd:: Canonical {? Structure } @qualid
 
-   This command declares :token:`qualid` as a canonical structure.
+   This command declares :token:`qualid` as a canonical instance of a
+   structure (a record).
 
    Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
    structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
@@ -1961,7 +1962,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
 
-         Canonical Structure nat_setoid.
+         Canonical nat_setoid.
 
       Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
       and :g:`B` can be synthesized in the next statement.
@@ -1978,11 +1979,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
-   .. cmdv:: Canonical Structure @ident {? : @type } := @term
+   .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
-      declaration :n:`Canonical Structure @ident`.
-
+      declaration :n:`Canonical @ident`.
 
 .. cmd:: Print Canonical Projections
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 191a4e9a20..d083d34b52 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
           Ssrview.AdaptorDb.declare k hints }
 END
 
-(** Canonical Structure alias *)
-
-GRAMMAR EXTEND Gram
-  GLOBAL: gallina_ext;
-
-  gallina_ext:
-      (* Canonical structure *)
-     [[ IDENT "Canonical"; qid = Constr.global ->
-          { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) }
-      | IDENT "Canonical"; ntn = Prim.by_notation ->
-          { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) }
-      | IDENT "Canonical"; qid = Constr.global;
-          d = G_vernac.def_body ->
-          { let s = coerce_reference_to_id qid in
-    Vernacexpr.VernacDefinition
-      ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((CAst.make (Name s)),None), d) }
-  ]];
-END
-
 (** Keyword compatibility fixes. *)
 
 (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
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}).
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 0664e18130..42bee25da3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -693,18 +693,20 @@ GRAMMAR EXTEND Gram
           LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] ->
             { VernacSetStrategy l }
       (* Canonical structure *)
-      | IDENT "Canonical"; IDENT "Structure"; qid = global ->
-          { VernacCanonical CAst.(make ~loc @@ AN qid) }
-      | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
+      | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
+          { match ud with
+           | None ->
+             VernacCanonical CAst.(make ~loc @@ AN qid)
+           | Some (u,d) ->
+             let s = coerce_reference_to_id qid in
+             VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) }
+      | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
           { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
-      | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
-          { let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),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) }