From 8549847fc7df04a4896dc2ff4b29eb54a867b4b2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 Jan 2019 13:44:38 +0100
Subject: refactor grammar

---
 vernac/g_vernac.mlg | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e7d81b8bb0..c36a6fa9c6 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -693,13 +693,15 @@ 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"; 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 ->
           { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
-      | 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)),u),d) }
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body ->
-- 
cgit v1.2.3