diff options
Diffstat (limited to 'grammar/q_util.mlp')
| -rw-r--r-- | grammar/q_util.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 6cdd2ec19..0b8d7fda7 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -75,7 +75,7 @@ let rec mlexpr_of_prod_entry_key f = function (** Keep in sync with Pcoq! *) assert (e = "tactic"); if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> - else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> |