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.

18 files changed, 32 insertions, 14 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 67c9dd0a3..03b49e333 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "ascii_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 open Pp
 open Errors
 open Util
diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib
deleted file mode 100644
index b00f92506..000000000
--- a/plugins/syntax/ascii_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Ascii_syntax
-Ascii_syntax_plugin_mod
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
new file mode 100644
index 000000000..7b9213a0e
--- /dev/null
+++ b/plugins/syntax/ascii_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Ascii_syntax
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index fe9386039..3142c8cf0 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "nat_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib
deleted file mode 100644
index 69b0cb20f..000000000
--- a/plugins/syntax/nat_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Nat_syntax
-Nat_syntax_plugin_mod
diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack
new file mode 100644
index 000000000..39bdd62f4
--- /dev/null
+++ b/plugins/syntax/nat_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Nat_syntax
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index fe9f1319e..57cb2f897 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "numbers_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
@@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n =
   let word = word_of_pos_bigint dloc h n in
   let args =
     if h < n_inlined then [word]
-    else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
+    else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
   in
   GApp (dloc, ref_constructor, args)
 
diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib
deleted file mode 100644
index ebc0bb202..000000000
--- a/plugins/syntax/numbers_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Numbers_syntax
-Numbers_syntax_plugin_mod
diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack
new file mode 100644
index 000000000..e48c00a0d
--- /dev/null
+++ b/plugins/syntax/numbers_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Numbers_syntax
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 05d73f9ec..3ae2d45f3 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -10,6 +10,10 @@ open Util
 open Names
 open Globnames
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "r_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib
deleted file mode 100644
index 5c173a140..000000000
--- a/plugins/syntax/r_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-R_syntax
-R_syntax_plugin_mod
diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack
new file mode 100644
index 000000000..d4ee75ea4
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mlpack
@@ -0,0 +1 @@
+R_syntax
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 2e696f391..de0fa77ef 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -7,10 +7,14 @@
 (***********************************************************************)
 
 open Globnames
-open Ascii_syntax
+open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
 open Coqlib
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "string_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_string
 
 (* make a string term from the string s *)
diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
deleted file mode 100644
index b108c9e00..000000000
--- a/plugins/syntax/string_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-String_syntax
-String_syntax_plugin_mod
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
new file mode 100644
index 000000000..45d6e0fa2
--- /dev/null
+++ b/plugins/syntax/string_syntax_plugin.mlpack
@@ -0,0 +1 @@
+String_syntax
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 53c1b5d7a..ce86c0a65 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -12,6 +12,10 @@ open Util
 open Names
 open Bigint
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "z_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib
deleted file mode 100644
index 36d41acc2..000000000
--- a/plugins/syntax/z_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Z_syntax
-Z_syntax_plugin_mod
diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack
new file mode 100644
index 000000000..411260c04
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Z_syntax