diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 16:30:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 16:49:13 +0100 |
| commit | cbc3a5f16871adb399689f7673a2a29a82dbf0cb (patch) | |
| tree | 4947075cc532172e4485e69aa67abae4c79e87ac /grammar | |
| parent | 8e77752080b6f0da3ce396e7537db9676e848a70 (diff) | |
All arguments defined through ARGUMENT EXTEND declare a tactic scope.
Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 7 |
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 |