diff options
| author | Emilio Jesus Gallego Arias | 2018-07-26 09:33:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-26 09:33:55 +0200 |
| commit | 6cd6f1edae2e2c7b2aaedd039b39caaf1d50aa9f (patch) | |
| tree | 684ba0dcb4d13196b80686d8672ba00928ea2fd9 | |
| parent | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (diff) | |
| parent | e17cbd44317f375e9a281a739facd19e118c1dba (diff) | |
Merge PR #8150: Fix static declaration of plugins in 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 |