aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/btauto_plugin.mlpack (renamed from plugins/btauto/btauto_plugin.mllib)1
-rw-r--r--plugins/cc/cc_plugin.mlpack (renamed from plugins/cc/cc_plugin.mllib)1
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack (renamed from plugins/decl_mode/decl_mode_plugin.mllib)1
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--plugins/derive/derive_plugin.mlpack (renamed from plugins/derive/derive_plugin.mllib)0
-rw-r--r--plugins/derive/g_derive.ml42
-rw-r--r--plugins/extraction/extraction_plugin.mlpack (renamed from plugins/extraction/extraction_plugin.mllib)1
-rw-r--r--plugins/extraction/g_extraction.ml42
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/firstorder/ground_plugin.mlpack (renamed from plugins/firstorder/ground_plugin.mllib)1
-rw-r--r--plugins/fourier/fourier_plugin.mlpack (renamed from plugins/fourier/fourier_plugin.mllib)1
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/funind/recdef_plugin.mlpack (renamed from plugins/funind/recdef_plugin.mllib)1
-rw-r--r--plugins/micromega/micromega_plugin.mlpack (renamed from plugins/micromega/micromega_plugin.mllib)1
-rw-r--r--plugins/nsatz/nsatz_plugin.mlpack (renamed from plugins/nsatz/nsatz_plugin.mllib)1
-rw-r--r--plugins/omega/omega_plugin.mlpack (renamed from plugins/omega/omega_plugin.mllib)1
-rw-r--r--plugins/quote/quote_plugin.mllib3
-rw-r--r--plugins/quote/quote_plugin.mlpack2
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/romega/romega_plugin.mlpack (renamed from plugins/romega/romega_plugin.mllib)1
-rw-r--r--plugins/rtauto/rtauto_plugin.mlpack (renamed from plugins/rtauto/rtauto_plugin.mllib)1
-rw-r--r--plugins/setoid_ring/newring.ml1
-rw-r--r--plugins/setoid_ring/newring_plugin.mllib3
-rw-r--r--plugins/setoid_ring/newring_plugin.mlpack2
-rw-r--r--plugins/syntax/ascii_syntax.ml4
-rw-r--r--plugins/syntax/ascii_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/ascii_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/nat_syntax.ml4
-rw-r--r--plugins/syntax/nat_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/nat_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/numbers_syntax.ml6
-rw-r--r--plugins/syntax/numbers_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/numbers_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/r_syntax.ml4
-rw-r--r--plugins/syntax/r_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/r_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/string_syntax.ml6
-rw-r--r--plugins/syntax/string_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/string_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/z_syntax.ml4
-rw-r--r--plugins/syntax/z_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/z_syntax_plugin.mlpack1
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