[ssr] move shorter Canonical to Coq proper

3 files changed, 8 insertions, 28 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 50a56f1d51..ca2d31d7ed 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.
@@ -1974,11 +1975,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/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index c36a6fa9c6..42bee25da3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -693,14 +693,14 @@ GRAMMAR EXTEND Gram
           LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] ->
             { VernacSetStrategy l }
       (* Canonical structure *)
-      | IDENT "Canonical"; IDENT "Structure"; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
+      | 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"; IDENT "Structure"; ntn = by_notation ->
+      | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
           { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
 
       (* Coercions *)