diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 17:19:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 18:22:38 +0200 |
| commit | 699b70cd9ad0d79cbde228bdb51fde224a3b524e (patch) | |
| tree | 0a542320b54ce277d8dcf3680a230a37f1271c8b /grammar | |
| parent | 16675c67c56456f6082c4da7c7657aaa2b1da375 (diff) | |
Moving Ltac-specific parsing API to ltac/ folder.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_util.mlp | 4 |
1 files changed, 2 insertions, 2 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, _) -> |