diff options
| author | Pierre-Marie Pédrot | 2018-07-25 17:48:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 17:48:45 +0200 |
| commit | e17cbd44317f375e9a281a739facd19e118c1dba (patch) | |
| tree | cf7955011a48ce3370b0ba0d8b28a13c3a45ad36 /coqpp | |
| parent | 523de4f878293cf1d582bd70300b34d497e705b3 (diff) | |
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.
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_main.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |