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/btauto/btauto_plugin.mllib | 3 --- plugins/btauto/btauto_plugin.mlpack | 2 ++ plugins/cc/cc_plugin.mllib | 5 ----- plugins/cc/cc_plugin.mlpack | 4 ++++ plugins/decl_mode/decl_mode_plugin.mllib | 6 ------ plugins/decl_mode/decl_mode_plugin.mlpack | 5 +++++ plugins/decl_mode/g_decl_mode.ml4 | 2 ++ plugins/derive/derive_plugin.mllib | 2 -- plugins/derive/derive_plugin.mlpack | 2 ++ plugins/derive/g_derive.ml4 | 2 ++ plugins/extraction/extraction_plugin.mllib | 12 ------------ plugins/extraction/extraction_plugin.mlpack | 11 +++++++++++ plugins/extraction/g_extraction.ml4 | 2 ++ plugins/firstorder/g_ground.ml4 | 2 ++ plugins/firstorder/ground_plugin.mllib | 8 -------- plugins/firstorder/ground_plugin.mlpack | 7 +++++++ plugins/fourier/fourier_plugin.mllib | 4 ---- plugins/fourier/fourier_plugin.mlpack | 3 +++ plugins/funind/recdef.ml | 2 +- plugins/funind/recdef_plugin.mllib | 11 ----------- plugins/funind/recdef_plugin.mlpack | 10 ++++++++++ plugins/micromega/micromega_plugin.mllib | 10 ---------- plugins/micromega/micromega_plugin.mlpack | 9 +++++++++ plugins/nsatz/nsatz_plugin.mllib | 6 ------ plugins/nsatz/nsatz_plugin.mlpack | 5 +++++ plugins/omega/omega_plugin.mllib | 4 ---- plugins/omega/omega_plugin.mlpack | 3 +++ plugins/quote/quote_plugin.mllib | 3 --- plugins/quote/quote_plugin.mlpack | 2 ++ plugins/romega/refl_omega.ml | 2 +- plugins/romega/romega_plugin.mllib | 4 ---- plugins/romega/romega_plugin.mlpack | 3 +++ plugins/rtauto/rtauto_plugin.mllib | 4 ---- plugins/rtauto/rtauto_plugin.mlpack | 3 +++ plugins/setoid_ring/newring.ml | 1 + plugins/setoid_ring/newring_plugin.mllib | 3 --- plugins/setoid_ring/newring_plugin.mlpack | 2 ++ plugins/syntax/ascii_syntax.ml | 4 ++++ plugins/syntax/ascii_syntax_plugin.mllib | 2 -- plugins/syntax/ascii_syntax_plugin.mlpack | 1 + plugins/syntax/nat_syntax.ml | 4 ++++ plugins/syntax/nat_syntax_plugin.mllib | 2 -- plugins/syntax/nat_syntax_plugin.mlpack | 1 + plugins/syntax/numbers_syntax.ml | 6 +++++- plugins/syntax/numbers_syntax_plugin.mllib | 2 -- plugins/syntax/numbers_syntax_plugin.mlpack | 1 + plugins/syntax/r_syntax.ml | 4 ++++ plugins/syntax/r_syntax_plugin.mllib | 2 -- plugins/syntax/r_syntax_plugin.mlpack | 1 + plugins/syntax/string_syntax.ml | 6 +++++- plugins/syntax/string_syntax_plugin.mllib | 2 -- plugins/syntax/string_syntax_plugin.mlpack | 1 + plugins/syntax/z_syntax.ml | 4 ++++ plugins/syntax/z_syntax_plugin.mllib | 2 -- plugins/syntax/z_syntax_plugin.mlpack | 1 + 55 files changed, 114 insertions(+), 101 deletions(-) delete mode 100644 plugins/btauto/btauto_plugin.mllib create mode 100644 plugins/btauto/btauto_plugin.mlpack delete mode 100644 plugins/cc/cc_plugin.mllib create mode 100644 plugins/cc/cc_plugin.mlpack delete mode 100644 plugins/decl_mode/decl_mode_plugin.mllib create mode 100644 plugins/decl_mode/decl_mode_plugin.mlpack delete mode 100644 plugins/derive/derive_plugin.mllib create mode 100644 plugins/derive/derive_plugin.mlpack delete mode 100644 plugins/extraction/extraction_plugin.mllib create mode 100644 plugins/extraction/extraction_plugin.mlpack delete mode 100644 plugins/firstorder/ground_plugin.mllib create mode 100644 plugins/firstorder/ground_plugin.mlpack delete mode 100644 plugins/fourier/fourier_plugin.mllib create mode 100644 plugins/fourier/fourier_plugin.mlpack delete mode 100644 plugins/funind/recdef_plugin.mllib create mode 100644 plugins/funind/recdef_plugin.mlpack delete mode 100644 plugins/micromega/micromega_plugin.mllib create mode 100644 plugins/micromega/micromega_plugin.mlpack delete mode 100644 plugins/nsatz/nsatz_plugin.mllib create mode 100644 plugins/nsatz/nsatz_plugin.mlpack delete mode 100644 plugins/omega/omega_plugin.mllib create mode 100644 plugins/omega/omega_plugin.mlpack delete mode 100644 plugins/quote/quote_plugin.mllib create mode 100644 plugins/quote/quote_plugin.mlpack delete mode 100644 plugins/romega/romega_plugin.mllib create mode 100644 plugins/romega/romega_plugin.mlpack delete mode 100644 plugins/rtauto/rtauto_plugin.mllib create mode 100644 plugins/rtauto/rtauto_plugin.mlpack delete mode 100644 plugins/setoid_ring/newring_plugin.mllib create mode 100644 plugins/setoid_ring/newring_plugin.mlpack delete mode 100644 plugins/syntax/ascii_syntax_plugin.mllib create mode 100644 plugins/syntax/ascii_syntax_plugin.mlpack delete mode 100644 plugins/syntax/nat_syntax_plugin.mllib create mode 100644 plugins/syntax/nat_syntax_plugin.mlpack delete mode 100644 plugins/syntax/numbers_syntax_plugin.mllib create mode 100644 plugins/syntax/numbers_syntax_plugin.mlpack delete mode 100644 plugins/syntax/r_syntax_plugin.mllib create mode 100644 plugins/syntax/r_syntax_plugin.mlpack delete mode 100644 plugins/syntax/string_syntax_plugin.mllib create mode 100644 plugins/syntax/string_syntax_plugin.mlpack delete mode 100644 plugins/syntax/z_syntax_plugin.mllib create mode 100644 plugins/syntax/z_syntax_plugin.mlpack (limited to 'plugins') diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mllib deleted file mode 100644 index 319a9c302..000000000 --- a/plugins/btauto/btauto_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Refl_btauto -G_btauto -Btauto_plugin_mod diff --git a/plugins/btauto/btauto_plugin.mlpack b/plugins/btauto/btauto_plugin.mlpack new file mode 100644 index 000000000..2410f906a --- /dev/null +++ b/plugins/btauto/btauto_plugin.mlpack @@ -0,0 +1,2 @@ +Refl_btauto +G_btauto diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib deleted file mode 100644 index 1bcfc5378..000000000 --- a/plugins/cc/cc_plugin.mllib +++ /dev/null @@ -1,5 +0,0 @@ -Ccalgo -Ccproof -Cctac -G_congruence -Cc_plugin_mod diff --git a/plugins/cc/cc_plugin.mlpack b/plugins/cc/cc_plugin.mlpack new file mode 100644 index 000000000..27e903fd3 --- /dev/null +++ b/plugins/cc/cc_plugin.mlpack @@ -0,0 +1,4 @@ +Ccalgo +Ccproof +Cctac +G_congruence diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib deleted file mode 100644 index 39342dbd1..000000000 --- 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 000000000..1b84a0790 --- /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 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.mllib deleted file mode 100644 index 5ee0fc6da..000000000 --- a/plugins/derive/derive_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Derive -G_derive diff --git a/plugins/derive/derive_plugin.mlpack b/plugins/derive/derive_plugin.mlpack new file mode 100644 index 000000000..5ee0fc6da --- /dev/null +++ b/plugins/derive/derive_plugin.mlpack @@ -0,0 +1,2 @@ +Derive +G_derive 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.mllib deleted file mode 100644 index ad3212434..000000000 --- a/plugins/extraction/extraction_plugin.mllib +++ /dev/null @@ -1,12 +0,0 @@ -Table -Mlutil -Modutil -Extraction -Common -Ocaml -Haskell -Scheme -Json -Extract_env -G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/extraction_plugin.mlpack b/plugins/extraction/extraction_plugin.mlpack new file mode 100644 index 000000000..9184f6501 --- /dev/null +++ b/plugins/extraction/extraction_plugin.mlpack @@ -0,0 +1,11 @@ +Table +Mlutil +Modutil +Extraction +Common +Ocaml +Haskell +Scheme +Json +Extract_env +G_extraction 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.mllib deleted file mode 100644 index 447a1fb51..000000000 --- a/plugins/firstorder/ground_plugin.mllib +++ /dev/null @@ -1,8 +0,0 @@ -Formula -Unify -Sequent -Rules -Instances -Ground -G_ground -Ground_plugin_mod diff --git a/plugins/firstorder/ground_plugin.mlpack b/plugins/firstorder/ground_plugin.mlpack new file mode 100644 index 000000000..65fb2e9a1 --- /dev/null +++ b/plugins/firstorder/ground_plugin.mlpack @@ -0,0 +1,7 @@ +Formula +Unify +Sequent +Rules +Instances +Ground +G_ground diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib deleted file mode 100644 index 0383b1a80..000000000 --- a/plugins/fourier/fourier_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Fourier -FourierR -G_fourier -Fourier_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack new file mode 100644 index 000000000..b6262f8ae --- /dev/null +++ b/plugins/fourier/fourier_plugin.mlpack @@ -0,0 +1,3 @@ +Fourier +FourierR +G_fourier 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.mllib deleted file mode 100644 index ec1f5436c..000000000 --- a/plugins/funind/recdef_plugin.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Indfun_common -Glob_termops -Recdef -Glob_term_to_relation -Functional_principles_proofs -Functional_principles_types -Invfun -Indfun -Merge -G_indfun -Recdef_plugin_mod diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack new file mode 100644 index 000000000..2b443f2a1 --- /dev/null +++ b/plugins/funind/recdef_plugin.mlpack @@ -0,0 +1,10 @@ +Indfun_common +Glob_termops +Recdef +Glob_term_to_relation +Functional_principles_proofs +Functional_principles_types +Invfun +Indfun +Merge +G_indfun diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib deleted file mode 100644 index f53a9e379..000000000 --- a/plugins/micromega/micromega_plugin.mllib +++ /dev/null @@ -1,10 +0,0 @@ -Sos_types -Mutils -Micromega -Polynomial -Mfourier -Certificate -Persistent_cache -Coq_micromega -G_micromega -Micromega_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mlpack b/plugins/micromega/micromega_plugin.mlpack new file mode 100644 index 000000000..ed253da3f --- /dev/null +++ b/plugins/micromega/micromega_plugin.mlpack @@ -0,0 +1,9 @@ +Sos_types +Mutils +Micromega +Polynomial +Mfourier +Certificate +Persistent_cache +Coq_micromega +G_micromega diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mllib deleted file mode 100644 index e991fb76f..000000000 --- a/plugins/nsatz/nsatz_plugin.mllib +++ /dev/null @@ -1,6 +0,0 @@ -Utile -Polynom -Ideal -Nsatz -G_nsatz -Nsatz_plugin_mod diff --git a/plugins/nsatz/nsatz_plugin.mlpack b/plugins/nsatz/nsatz_plugin.mlpack new file mode 100644 index 000000000..b55adf43c --- /dev/null +++ b/plugins/nsatz/nsatz_plugin.mlpack @@ -0,0 +1,5 @@ +Utile +Polynom +Ideal +Nsatz +G_nsatz diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib deleted file mode 100644 index 2b387fdce..000000000 --- a/plugins/omega/omega_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Omega -Coq_omega -G_omega -Omega_plugin_mod diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack new file mode 100644 index 000000000..df7f1047f --- /dev/null +++ b/plugins/omega/omega_plugin.mlpack @@ -0,0 +1,3 @@ +Omega +Coq_omega +G_omega 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.mllib deleted file mode 100644 index 1625009d0..000000000 --- a/plugins/romega/romega_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Const_omega -Refl_omega -G_romega -Romega_plugin_mod diff --git a/plugins/romega/romega_plugin.mlpack b/plugins/romega/romega_plugin.mlpack new file mode 100644 index 000000000..38d0e9411 --- /dev/null +++ b/plugins/romega/romega_plugin.mlpack @@ -0,0 +1,3 @@ +Const_omega +Refl_omega +G_romega diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib deleted file mode 100644 index 0e3460449..000000000 --- a/plugins/rtauto/rtauto_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Proof_search -Refl_tauto -G_rtauto -Rtauto_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mlpack b/plugins/rtauto/rtauto_plugin.mlpack new file mode 100644 index 000000000..61c5e945b --- /dev/null +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -0,0 +1,3 @@ +Proof_search +Refl_tauto +G_rtauto 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 -- cgit v1.2.3