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. --- grammar/q_util.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'grammar/q_util.mli') diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 837ec6fb0..712aa8509 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -28,6 +28,6 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr val mlexpr_of_ident : string -> MLast.expr -val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type -- cgit v1.2.3