From 0f2475ae87a89344a50b323e47765b61e3e3eb59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Feb 2014 20:52:44 +0100
Subject: 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.

---
 grammar/vernacextend.ml4 | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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