diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520bc..de701bb239 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -12,9 +12,10 @@ open Pp open Genarg open Stdarg open Constrarg +open Tacarg open Extraargs open Pcoq.Prim -open Pcoq.Tactic +open Pltac open Mod_subst open Names open Tacexpr @@ -53,7 +54,7 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) -let clause = Pcoq.Tactic.clause_dft_concl +let clause = Pltac.clause_dft_concl TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] @@ -983,7 +984,7 @@ let pr_cmp' _prc _prlc _prt = pr_cmp let pr_test_gen f (Test(c,x,y)) = Pp.(f x ++ pr_cmp c ++ f y) -let pr_test = pr_test_gen (Pptactic.pr_or_var Pp.int) +let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) let pr_test' _prc _prlc _prt = pr_test |