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

---
 plugins/ssr/ssrvernac.mlg | 20 --------------------
 1 file changed, 20 deletions(-)

(limited to 'plugins')

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