diff options
Diffstat (limited to 'ltac/extraargs.ml4')
| -rw-r--r-- | ltac/extraargs.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index c6d72e03e..c32f757d9 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -35,11 +35,11 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr -let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Constrarg.wit_intro_pattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) (** Backward-compatible tactic notation entry names *) |