diff options
| -rw-r--r-- | grammar/vernacextend.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
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 >>; ] ] ] ; |