diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d6ba670d8..23ce5fb4e 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -11,10 +11,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 @@ -27,7 +27,6 @@ open Equality open Misctypes open Sigma.Notations open Proofview.Notations -open Constrarg DECLARE PLUGIN "extratactics" @@ -53,7 +52,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) ] @@ -984,7 +983,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 |