diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index a1b3f4f25..175853d50 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -61,7 +61,7 @@ let rec mlexpr_of_symbol = function <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> | Uentryl (e, l) -> assert (e = "tactic"); - let arg = get_argt <:expr< Constrarg.wit_tactic >> in + let arg = get_argt <:expr< Tacarg.wit_tactic >> in <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> let make_prod_item = function |