diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_util.mlp | 4 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 2d5c40894..919ca3ad7 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -70,8 +70,8 @@ let rec mlexpr_of_prod_entry_key f = function | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry (Pltac.binder_tactic) >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 683a7e2f7..fe864ed40 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 |