Merge branch 'pack-plugins'

42 files changed, 47 insertions, 34 deletions

diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack
index 319a9c302a..2410f906a3 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 1bcfc5378b..27e903fd38 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 39342dbd1c..1b84a0790f 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 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
diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack
index 5ee0fc6da6..5ee0fc6da6 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 39cad4d03c..d4dc7e0eed 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 ad32124347..9184f65017 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 0a8cb0ccd3..19fda4aead 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 a78532e339..cec3505a97 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 447a1fb513..65fb2e9a1d 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 0383b1a80b..b6262f8aeb 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 80866e8b8c..95b4967faa 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 ec1f5436ca..2b443f2a1b 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 f53a9e3797..ed253da3fd 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 e991fb76f7..b55adf43c0 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 2b387fdcee..df7f1047f2 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 d1b3ccbe1e..0000000000
--- 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 0000000000..2e9be09d8d
--- /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 007a9ec673..a059512d84 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 1625009d06..38d0e94111 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 0e34604495..61c5e945bc 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 154ec6e1bf..7af72b07cf 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 7d6c495889..0000000000
--- 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 0000000000..23663b4090
--- /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 67c9dd0a38..03b49e3336 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 b00f92506e..0000000000
--- 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 0000000000..7b9213a0e2
--- /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 fe9386039f..3142c8cf00 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 69b0cb20f6..0000000000
--- 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 0000000000..39bdd62f47
--- /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 fe9f1319eb..57cb2f897a 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 ebc0bb2022..0000000000
--- 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 0000000000..e48c00a0d0
--- /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 05d73f9ec1..3ae2d45f32 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 5c173a140f..0000000000
--- 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 0000000000..d4ee75ea48
--- /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 2e696f391f..de0fa77eff 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 b108c9e007..0000000000
--- 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 0000000000..45d6e0fa23
--- /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 53c1b5d7a0..ce86c0a65f 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 36d41acc20..0000000000
--- 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 0000000000..411260c04c
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Z_syntax