From e17cbd44317f375e9a281a739facd19e118c1dba Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 25 Jul 2018 17:48:45 +0200
Subject: Fix static declaration of plugins in coqpp.

The module was not properly registered with dynlink turned off, leading to
a failure of compilation of the prelude.
---
 coqpp/coqpp_main.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index e76a1e9ed8..fd425ef4ff 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -326,10 +326,14 @@ let print_ast fmt ext =
 
 end
 
+let declare_plugin fmt name =
+  fprintf fmt "let %s = \"%s\"@\n" plugin_name name;
+  fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name
+
 let pr_ast fmt = function
 | Code s -> fprintf fmt "%s@\n" s.code
 | Comment s -> fprintf fmt "%s@\n" s
-| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name
+| DeclarePlugin name -> declare_plugin fmt name
 | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
 | VernacExt -> fprintf fmt "VERNACEXT@\n"
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
-- 
cgit v1.2.3