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.

42 files changed, 47 insertions, 34 deletions

diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack
index 319a9c302..2410f906a 100644
--- a/plugins/btauto/btauto_plugin.mllib
+++ b/plugins/btauto/btauto_plugin.mlpack
@@ -1,3 +1,2 @@
 Refl_btauto
 G_btauto
-Btauto_plugin_mod
diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack
index 1bcfc5378..27e903fd3 100644
--- a/plugins/cc/cc_plugin.mllib
+++ b/plugins/cc/cc_plugin.mlpack
@@ -2,4 +2,3 @@ Ccalgo
 Ccproof
 Cctac
 G_congruence
-Cc_plugin_mod
diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack
index 39342dbd1..1b84a0790 100644
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ b/plugins/decl_mode/decl_mode_plugin.mlpack
@@ -3,4 +3,3 @@ Decl_interp
 Decl_proof_instr
 Ppdecl_proof
 G_decl_mode
-Decl_mode_plugin_mod
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143d..0feba6365 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
diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack
index 5ee0fc6da..5ee0fc6da 100644
--- a/plugins/derive/derive_plugin.mllib
+++ b/plugins/derive/derive_plugin.mlpack
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 39cad4d03..d4dc7e0ee 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -10,6 +10,8 @@ open Constrarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "derive_plugin"
+
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack
index ad3212434..9184f6501 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -9,4 +9,3 @@ Scheme
 Json
 Extract_env
 G_extraction
-Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 0a8cb0ccd..19fda4aea 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "extraction_plugin"
+
 (* ML names *)
 
 open Genarg
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index a78532e33..cec3505a9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -153,6 +153,8 @@ TACTIC EXTEND gintuition
 END
 
 open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
 
 let default_declarative_automation =
   Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack
index 447a1fb51..65fb2e9a1 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mlpack
@@ -5,4 +5,3 @@ Rules
 Instances
 Ground
 G_ground
-Ground_plugin_mod
diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack
index 0383b1a80..b6262f8ae 100644
--- a/plugins/fourier/fourier_plugin.mllib
+++ b/plugins/fourier/fourier_plugin.mlpack
@@ -1,4 +1,3 @@
 Fourier
 FourierR
 G_fourier
-Fourier_plugin_mod
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 80866e8b8..95b4967fa 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in 
+    let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack
index ec1f5436c..2b443f2a1 100644
--- a/plugins/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -8,4 +8,3 @@ Invfun
 Indfun
 Merge
 G_indfun
-Recdef_plugin_mod
diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack
index f53a9e379..ed253da3f 100644
--- a/plugins/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mlpack
@@ -7,4 +7,3 @@ Certificate
 Persistent_cache
 Coq_micromega
 G_micromega
-Micromega_plugin_mod
diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack
index e991fb76f..b55adf43c 100644
--- a/plugins/nsatz/nsatz_plugin.mllib
+++ b/plugins/nsatz/nsatz_plugin.mlpack
@@ -3,4 +3,3 @@ Polynom
 Ideal
 Nsatz
 G_nsatz
-Nsatz_plugin_mod
diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mlpack
index 2b387fdce..df7f1047f 100644
--- a/plugins/omega/omega_plugin.mllib
+++ b/plugins/omega/omega_plugin.mlpack
@@ -1,4 +1,3 @@
 Omega
 Coq_omega
 G_omega
-Omega_plugin_mod
diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
deleted file mode 100644
index d1b3ccbe1..000000000
--- a/plugins/quote/quote_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Quote
-G_quote
-Quote_plugin_mod
diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack
new file mode 100644
index 000000000..2e9be09d8
--- /dev/null
+++ b/plugins/quote/quote_plugin.mlpack
@@ -0,0 +1,2 @@
+Quote
+G_quote
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 007a9ec67..a059512d8 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -9,7 +9,7 @@
 open Pp
 open Util
 open Const_omega
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
 (* \section{Useful functions and flags} *)
diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack
index 1625009d0..38d0e9411 100644
--- a/plugins/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mlpack
@@ -1,4 +1,3 @@
 Const_omega
 Refl_omega
 G_romega
-Romega_plugin_mod
diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mlpack
index 0e3460449..61c5e945b 100644
--- a/plugins/rtauto/rtauto_plugin.mllib
+++ b/plugins/rtauto/rtauto_plugin.mlpack
@@ -1,4 +1,3 @@
 Proof_search
 Refl_tauto
 G_rtauto
-Rtauto_plugin_mod
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 154ec6e1b..7af72b07c 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -106,6 +106,7 @@ let protect_tac_in map id =
 (****************************************************************************)
 
 let closed_term t l =
+  let open Quote_plugin in
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
deleted file mode 100644
index 7d6c49588..000000000
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Newring
-Newring_plugin_mod
-G_newring
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
new file mode 100644
index 000000000..23663b409
--- /dev/null
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -0,0 +1,2 @@
+Newring
+G_newring
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