diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 16:57:05 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 21:08:26 +0100 |
commit | 4b2cdf733df6dc23247b078679e71da98e54f5cc (patch) | |
tree | ac05560456999b14a897e1701ae6678ab5c6e6b7 /plugins | |
parent | 4d13842869647790c9bd3084dce672fee7b648a1 (diff) |
Removing the special status of generic entries defined by Coq itself.
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/cc/g_congruence.ml4 | 4 | ||||
-rw-r--r-- | plugins/derive/g_derive.ml4 | 4 | ||||
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 4 | ||||
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 4 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 4 | ||||
-rw-r--r-- | plugins/omega/g_omega.ml4 | 2 | ||||
-rw-r--r-- | plugins/quote/g_quote.ml4 | 4 | ||||
-rw-r--r-- | plugins/romega/g_romega.ml4 | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 5 |
10 files changed, 37 insertions, 0 deletions
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 5dbc340ca..9a53e2e16 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -9,6 +9,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Cctac +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr DECLARE PLUGIN "cc_plugin" diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 18570a684..35a5a7616 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Constrarg +open Pcoq.Prim +open Pcoq.Constr + (*i camlp4deps: "grammar/grammar.cma" i*) let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index aec958689..7bd07f625 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -11,6 +11,10 @@ (* ML names *) open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr open Pp open Names open Nameops diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3e8be3699..587d10d1c 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,6 +15,10 @@ open Goptions open Tacticals open Tacinterp open Libnames +open Constrarg +open Stdarg +open Pcoq.Prim +open Pcoq.Tactic DECLARE PLUGIN "ground_plugin" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index dbcdeb83a..4bd69b9fe 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -16,8 +16,12 @@ open Constrexpr open Indfun_common open Indfun open Genarg +open Constrarg open Tacticals open Misctypes +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "recdef_plugin" diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index bfc9c727d..bca1c2feb 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -18,6 +18,10 @@ open Errors open Misctypes +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Tactic DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 04c62eb48..b314e0d85 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin" open Names open Coq_omega +open Constrarg +open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 7a3d7936a..a15b0eb05 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,6 +13,10 @@ open Misctypes open Tacexpr open Geninterp open Quote +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "quote_plugin" diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 6b2b2bbfa..61efa9f54 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega +open Constrarg +open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 856ec0db5..cd1d704dd 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -14,6 +14,11 @@ open Libnames open Printer open Newring_ast open Newring +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "newring_plugin" |