diff options
| -rw-r--r-- | grammar/vernacextend.ml4 | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 4337793022..3a99916331 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -125,7 +125,13 @@ EXTEND | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; OPT "|"; l = LIST1 rule SEP "|"; "END" -> - declare_command loc s c <:expr<Some $lid:nt$>> l ] ] + declare_command loc s c <:expr<Some $lid:nt$>> l + | "DECLARE"; "PLUGIN"; name = STRING -> + declare_str_items loc [ + <:str_item< value __coq_plugin_name = $str:name$ >>; + <:str_item< value _ = Mltop.add_known_module $str:name$ >>; + ] + ] ] ; classification: [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> |