From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 17:34:12 +0200 Subject: Moving the Ltac plugin to a pack-based one. This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements. --- plugins/btauto/g_btauto.ml4 | 2 ++ plugins/cc/g_congruence.ml4 | 1 + plugins/decl_mode/decl_interp.ml | 1 + plugins/decl_mode/decl_proof_instr.ml | 1 + plugins/decl_mode/g_decl_mode.ml4 | 1 + plugins/decl_mode/ppdecl_proof.ml | 1 + plugins/extraction/g_extraction.ml4 | 1 + plugins/firstorder/g_ground.ml4 | 1 + plugins/firstorder/ground.ml | 1 + plugins/fourier/g_fourier.ml4 | 1 + plugins/funind/g_indfun.ml4 | 1 + plugins/funind/invfun.ml | 1 + plugins/ltac/ltac_plugin.mllib | 27 --------------------------- plugins/ltac/ltac_plugin.mlpack | 27 +++++++++++++++++++++++++++ plugins/micromega/g_micromega.ml4 | 1 + plugins/nsatz/g_nsatz.ml4 | 4 ++-- plugins/omega/g_omega.ml4 | 1 + plugins/quote/g_quote.ml4 | 1 + plugins/romega/g_romega.ml4 | 1 + plugins/rtauto/g_rtauto.ml4 | 2 ++ plugins/rtauto/refl_tauto.ml | 1 + plugins/setoid_ring/g_newring.ml4 | 1 + plugins/setoid_ring/newring.ml | 1 + plugins/ssrmatching/ssrmatching.ml4 | 1 + 24 files changed, 52 insertions(+), 29 deletions(-) delete mode 100644 plugins/ltac/ltac_plugin.mllib create mode 100644 plugins/ltac/ltac_plugin.mlpack (limited to 'plugins') diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index f3e2c99f4..298027448 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 6f6811334..7e76854b1 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index f68c01b18..2b63ed6d6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Names diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e19dc86c4..deb2ede1d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Pp diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 18a35c6cf..a71d20f0d 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "decl_mode_plugin" +open Ltac_plugin open Compat open Pp open Decl_expr diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 59a0bb5a2..f5de638ed 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Pp open Decl_expr diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index e1d6bb4a8..3ed959cf2 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin" (* ML names *) +open Ltac_plugin open Genarg open Stdarg open Pcoq.Prim diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 260e86ad6..e28d6aa62 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Formula open Sequent open Ground diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 628af4e71..d6cd7e2a0 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Formula open Sequent open Rules diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 7c665ae7b..1960fa835 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open FourierR DECLARE PLUGIN "fourier_plugin" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6603a95a8..368b23be3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Compat open Util open Term diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e4833..70333b063 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Tacexpr open Declarations open CErrors diff --git a/plugins/ltac/ltac_plugin.mllib b/plugins/ltac/ltac_plugin.mllib deleted file mode 100644 index af1c7149d..000000000 --- a/plugins/ltac/ltac_plugin.mllib +++ /dev/null @@ -1,27 +0,0 @@ -Tacarg -Pptactic -Pltac -Taccoerce -Tacsubst -Tacenv -Tactic_debug -Tacintern -Tacentries -Profile_ltac -Tactic_matching -Tacinterp -Evar_tactics -Tactic_option -Extraargs -G_obligations -Coretactics -Extratactics -Profile_ltac_tactics -G_auto -G_class -Rewrite -G_rewrite -Tauto -G_eqdecide -G_tactic -G_ltac diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack new file mode 100644 index 000000000..af1c7149d --- /dev/null +++ b/plugins/ltac/ltac_plugin.mlpack @@ -0,0 +1,27 @@ +Tacarg +Pptactic +Pltac +Taccoerce +Tacsubst +Tacenv +Tactic_debug +Tacintern +Tacentries +Profile_ltac +Tactic_matching +Tacinterp +Evar_tactics +Tactic_option +Extraargs +G_obligations +Coretactics +Extratactics +Profile_ltac_tactics +G_auto +G_class +Rewrite +G_rewrite +Tauto +G_eqdecide +G_tactic +G_ltac diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 79020ed03..ccb6daa11 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,6 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 5f906a8da..195dec362 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -1,5 +1,3 @@ -DECLARE PLUGIN "nsatz_plugin" - (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (*