From d66fe71c93bc06f6006c64118deb1d5b01bf7487 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:01:23 +0100 Subject: Adding a universe argument to Pcoq.create_generic_entry. --- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/funind/g_indfun.ml4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 2d096a1081..2afbaca2c8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry = Gram.entry_create "vernac:proof_command" (* Auxiliary grammar entry. *) let proof_instr : raw_proof_instr Gram.entry = - Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr) + Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr) let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61ada5cc8c..dbcdeb83ad 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -149,7 +149,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) GEXTEND Gram GLOBAL: function_rec_definition_loc ; -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: 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. --- plugins/cc/g_congruence.ml4 | 4 ++++ plugins/derive/g_derive.ml4 | 4 ++++ plugins/extraction/g_extraction.ml4 | 4 ++++ plugins/firstorder/g_ground.ml4 | 4 ++++ plugins/funind/g_indfun.ml4 | 4 ++++ plugins/micromega/g_micromega.ml4 | 4 ++++ plugins/omega/g_omega.ml4 | 2 ++ plugins/quote/g_quote.ml4 | 4 ++++ plugins/romega/g_romega.ml4 | 2 ++ plugins/setoid_ring/g_newring.ml4 | 5 +++++ 10 files changed, 37 insertions(+) (limited to 'plugins') diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 5dbc340caa..9a53e2e16a 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 18570a6846..35a5a7616c 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 aec9586895..7bd07f6255 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 3e8be36993..587d10d1cc 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 dbcdeb83ad..4bd69b9fe7 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 bfc9c727d5..bca1c2febd 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 04c62eb487..b314e0d85f 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 7a3d7936a6..a15b0eb05a 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 6b2b2bbfaf..61efa9f545 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 856ec0db5f..cd1d704dde 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" -- cgit v1.2.3 From 36e865119e5bb5fbaed14428fc89ecd4e96fb7be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 18:27:39 +0100 Subject: Removing the special status of generic arguments defined by Coq itself. This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4bd69b9fe7..e93c395e3d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -94,7 +94,7 @@ let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." -ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END -- cgit v1.2.3