From ce84f518a210237804779c8840b2783e1f5d8e56 Mon Sep 17 00:00:00 2001
From: Matej Kosik <matej.kosik@inria.fr>
Date: Sat, 27 May 2017 22:05:03 +0200
Subject: make the expansion of the "DECLARE PLUGIN" closer to the way how a
 human would write that code

---
 grammar/vernacextend.mlp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 4f9a7c75c..798b46523 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -143,7 +143,7 @@ EXTEND
       | "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$ >>;
+          <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
         ]
       ] ]
   ;
-- 
cgit v1.2.3