aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.ml47
1 files changed, 5 insertions, 2 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 13f761113..65dc237bb 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -231,8 +231,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
<:str_item< do {
Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
Pptactic.declare_extra_genarg_pprule
- $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ }
- >> ]
+ $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
+ Egramcoq.create_ltac_quotation $se$
+ (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v))
+ ($lid:s$, None)
+ } >> ]
let declare_vernac_argument loc s pr cl =
let se = mlexpr_of_string s in