diff options
Diffstat (limited to 'src/g_ltac2.ml4')
| -rw-r--r-- | src/g_ltac2.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index c738cb65bd..31eb6d9db5 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -91,8 +91,7 @@ let tac2def_mut = Gram.entry_create "tactic:tac2def_mut" let tac2def_run = Gram.entry_create "tactic:tac2def_run" let tac2mode = Gram.entry_create "vernac:ltac2_command" -(** FUCK YOU API *) -let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry) +let ltac1_expr = Pltac.tactic_expr let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x) let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c |