diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 30 |
1 files changed, 13 insertions, 17 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f3482c31..891e2dba 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,26 +21,22 @@ open Util open Evd open Equality open Misctypes -open Proofview.Notations DECLARE PLUGIN "extratactics" (**********************************************************************) -(* admit, replace, discriminate, injection, simplify_eq *) +(* replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) -TACTIC EXTEND admit - [ "admit" ] -> [ admit_as_an_axiom ] -END - -let replace_in_clause_maybe_by (sigma,c1) c2 cl tac = - Proofview.Unsafe.tclEVARS sigma <*> - (replace_in_clause_maybe_by c1 c2 cl) - (Option.map Tacinterp.eval_tactic tac) +let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = + Tacticals.New.tclWITHHOLES false + (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac)) + sigma1 let replace_term dir_opt (sigma,c) cl = - Proofview.Unsafe.tclEVARS sigma <*> - (replace_term dir_opt c) cl + Tacticals.New.tclWITHHOLES false + (replace_term dir_opt c cl) + sigma TACTIC EXTEND replace ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] @@ -71,8 +67,8 @@ let induction_arg_of_quantified_hyp = function ElimOnIdent and not as "constr" *) let elimOnConstrWithHoles tac with_evars c = - Tacticals.New.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (None,ElimOnConstr c.it)) + Tacticals.New.tclWITHHOLES with_evars + (tac with_evars (Some (None,ElimOnConstr c.it))) c.sigma TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> @@ -202,7 +198,7 @@ END let onSomeWithHoles tac = function | None -> tac None - | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it) + | Some c -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma TACTIC EXTEND contradiction [ "contradiction" constr_with_bindings_opt(c) ] -> @@ -246,8 +242,8 @@ END let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - Proofview.Unsafe.tclEVARS sigma <*> - general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true + Tacticals.New.tclWITHHOLES false + (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) sigma TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> |