diff options
| author | Maxime Dénès | 2019-02-13 21:53:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-13 21:53:15 +0100 |
| commit | 64eaf184df8ca52b7254a03e3b4f87c3c0491fdd (patch) | |
| tree | 4abe81d9b619baeeb844a3a3b653a27086ddbf67 /plugins | |
| parent | aa2d7486702433c94bfd645d3a5f6575a9ee729f (diff) | |
| parent | 737ae4816a9c84369bc1c0a0b359a9fd4f63dbe6 (diff) | |
Merge PR #9450: Fix #9432: canonical structure and coercion accept universe binders.
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
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 *) |