diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-15 20:52:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-12 14:01:10 +0200 |
| commit | 0f2475ae87a89344a50b323e47765b61e3e3eb59 (patch) | |
| tree | 4b628d6578463731ddfdd046bf9433b27ee92cbe /grammar/vernacextend.ml4 | |
| parent | 9f8d5a9bcae4c4ca4d761e7ae0c2fdc99bcb1340 (diff) | |
Plugin names must be declared in the header of .ml4 file, be they static or
dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
Diffstat (limited to 'grammar/vernacextend.ml4')
| -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 433779302..3a9991633 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$ >> |