From 454816235038540977826f1ab7ba96005639f5e1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 29 Jan 2019 15:44:33 +0100
Subject: Fix #9432: canonical structure and coercion accept universe binders.

(when defining a new constant)
---
 vernac/g_vernac.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

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) }
-- 
cgit v1.2.3


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(-)

(limited to 'vernac')

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


From 737ae4816a9c84369bc1c0a0b359a9fd4f63dbe6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 13 Feb 2019 13:53:34 +0100
Subject: [ssr] move shorter Canonical to Coq proper

---
 vernac/g_vernac.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

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 *)
-- 
cgit v1.2.3