From 509c30c93dca8ca8c78f1da1eefc056226d90346 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 1 Jun 2016 12:03:35 +0200
Subject: Compilation via pack for plugins of the stdlib

 For now, the pack name reuse the previous .cma name of the plugin,
 (extraction_plugin, etc).

 The earlier .mllib files in plugins are now named .mlpack.
 They are also handled by bin/ocamllibdep, just as .mllib.
 We've slightly modified ocamllibdep to help setting the -for-pack
 options: in *.mlpack.d files, there are some extra variables such as
  foo/bar_FORPACK := -for-pack Baz
 when foo/bar.ml is mentioned in baz.mlpack.

 When a plugin is calling a function from another plugin, the name
 need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).

 Btw, we discard the generated files plugins/*/*_mod.ml, they are
 obsolete now, replaced by DECLARE PLUGIN.

 Nota: there's a potential problem in the micromega directory,
 some .ml files are linked both in micromega_plugin and in csdpcert.
 And we now compile these files with a -for-pack, even if they are
 not packed in the case of csdpcert. In practice, csdpcert seems
 to work well, but we should verify with OCaml experts.
---
 plugins/decl_mode/decl_mode_plugin.mllib  | 6 ------
 plugins/decl_mode/decl_mode_plugin.mlpack | 5 +++++
 plugins/decl_mode/g_decl_mode.ml4         | 2 ++
 3 files changed, 7 insertions(+), 6 deletions(-)
 delete mode 100644 plugins/decl_mode/decl_mode_plugin.mllib
 create mode 100644 plugins/decl_mode/decl_mode_plugin.mlpack

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib
deleted file mode 100644
index 39342dbd1c..0000000000
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ /dev/null
@@ -1,6 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode
-Decl_mode_plugin_mod
diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
new file mode 100644
index 0000000000..1b84a0790f
--- /dev/null
+++ b/plugins/decl_mode/decl_mode_plugin.mlpack
@@ -0,0 +1,5 @@
+Decl_mode
+Decl_interp
+Decl_proof_instr
+Ppdecl_proof
+G_decl_mode
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143df..0feba6365c 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "decl_mode_plugin"
+
 open Compat
 open Pp
 open Decl_expr
-- 
cgit v1.2.3