diff options
Diffstat (limited to 'plugins')
47 files changed, 51 insertions, 130 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/plugins.itarget b/plugins/plugins.itarget deleted file mode 100644 index 56aa42b069..0000000000 --- a/plugins/plugins.itarget +++ /dev/null @@ -1,3 +0,0 @@ -pluginsopt.otarget -pluginsbyte.otarget -pluginsvo.otarget
\ No newline at end of file diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget deleted file mode 100644 index d8752f8b80..0000000000 --- a/plugins/pluginsbyte.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cma -setoid_ring/newring_plugin.cma -extraction/extraction_plugin.cma -decl_mode/decl_mode_plugin.cma -firstorder/ground_plugin.cma -rtauto/rtauto_plugin.cma -fourier/fourier_plugin.cma -romega/romega_plugin.cma -omega/omega_plugin.cma -micromega/micromega_plugin.cma -cc/cc_plugin.cma -nsatz/nsatz_plugin.cma -funind/recdef_plugin.cma -syntax/ascii_syntax_plugin.cma -syntax/nat_syntax_plugin.cma -syntax/numbers_syntax_plugin.cma -syntax/r_syntax_plugin.cma -syntax/string_syntax_plugin.cma -syntax/z_syntax_plugin.cma -quote/quote_plugin.cma -derive/derive_plugin.cma
\ No newline at end of file diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget deleted file mode 100644 index 220e5182d9..0000000000 --- a/plugins/pluginsdyn.itarget +++ /dev/null @@ -1,24 +0,0 @@ -btauto/btauto_plugin.cmxs -field/field_plugin.cmxs -setoid_ring/newring_plugin.cmxs -extraction/extraction_plugin.cmxs -decl_mode/decl_mode_plugin.cmxs -firstorder/ground_plugin.cmxs -rtauto/rtauto_plugin.cmxs -fourier/fourier_plugin.cmxs -romega/romega_plugin.cmxs -omega/omega_plugin.cmxs -micromega/micromega_plugin.cmxs -subtac/subtac_plugin.cmxs -ring/ring_plugin.cmxs -cc/cc_plugin.cmxs -nsatz/nsatz_plugin.cmxs -funind/recdef_plugin.cmxs -syntax/ascii_syntax_plugin.cmxs -syntax/nat_syntax_plugin.cmxs -syntax/numbers_syntax_plugin.cmxs -syntax/r_syntax_plugin.cmxs -syntax/string_syntax_plugin.cmxs -syntax/z_syntax_plugin.cmxs -quote/quote_plugin.cmxs -derive/derive_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget deleted file mode 100644 index 04a1e711cb..0000000000 --- a/plugins/pluginsopt.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cmxa -setoid_ring/newring_plugin.cmxa -extraction/extraction_plugin.cmxa -decl_mode/decl_mode_plugin.cmxa -firstorder/ground_plugin.cmxa -rtauto/rtauto_plugin.cmxa -fourier/fourier_plugin.cmxa -romega/romega_plugin.cmxa -omega/omega_plugin.cmxa -micromega/micromega_plugin.cmxa -cc/cc_plugin.cmxa -nsatz/nsatz_plugin.cmxa -funind/recdef_plugin.cmxa -syntax/ascii_syntax_plugin.cmxa -syntax/nat_syntax_plugin.cmxa -syntax/numbers_syntax_plugin.cmxa -syntax/r_syntax_plugin.cmxa -syntax/string_syntax_plugin.cmxa -syntax/z_syntax_plugin.cmxa -quote/quote_plugin.cmxa -derive/derive_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget deleted file mode 100644 index a59bf29c98..0000000000 --- a/plugins/pluginsvo.itarget +++ /dev/null @@ -1,12 +0,0 @@ -btauto/vo.otarget -fourier/vo.otarget -funind/vo.otarget -nsatz/vo.otarget -micromega/vo.otarget -omega/vo.otarget -quote/vo.otarget -romega/vo.otarget -rtauto/vo.otarget -setoid_ring/vo.otarget -extraction/vo.otarget -derive/vo.otarget
\ No newline at end of file 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..57ef920325 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None @@ -106,6 +95,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 |