diff options
Diffstat (limited to 'grammar/q_util.ml4')
| -rw-r--r-- | grammar/q_util.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index c529260e9d..05c94394d3 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -71,8 +71,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.name_of_entry Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> + else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> |