diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index be8390c95..d16ed84a2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -14,7 +14,7 @@ open Stdarg open Constrarg open Extraargs open Pcoq.Prim -open Pcoq.Tactic +open Pltac open Mod_subst open Names open Tacexpr @@ -53,7 +53,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) ] |