diff options
| author | Enrico Tassi | 2019-02-13 13:53:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-13 14:12:03 +0100 |
| commit | 737ae4816a9c84369bc1c0a0b359a9fd4f63dbe6 (patch) | |
| tree | ed34675a9b0c837c82ac0251e4dbf1f45bce02d9 /plugins | |
| parent | 1123165d3186124bd0b72b382d39383aefe347d8 (diff) | |
[ssr] move shorter Canonical to Coq proper
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 20 |
1 files changed, 0 insertions, 20 deletions
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 *) |