aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/coretactics.ml412
-rw-r--r--tactics/extratactics.ml418
-rw-r--r--tactics/tacinterp.ml21
-rw-r--r--tactics/tactics.ml3
4 files changed, 25 insertions, 29 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 179d3622f..cbac5c73a 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -12,6 +12,8 @@ open Util
open Locus
open Misctypes
+open Proofview.Notations
+
DECLARE PLUGIN "coretactics"
TACTIC EXTEND reflexivity
@@ -67,7 +69,7 @@ END
TACTIC EXTEND left_with
[ "left" "with" bindings(bl) ] -> [
let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false) sigma bl
+ Proofview.V82.tclEVARS sigma <*> Tactics.left_with_bindings false bl
]
END
@@ -91,7 +93,7 @@ END
TACTIC EXTEND right_with
[ "right" "with" bindings(bl) ] -> [
let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false) sigma bl
+ Proofview.V82.tclEVARS sigma <*> Tactics.right_with_bindings false bl
]
END
@@ -114,7 +116,7 @@ TACTIC EXTEND constructor
let { Evd.sigma = sigma; it = bl } = bl in
let i = Tacinterp.interp_int_or_var ist i in
let tac c = Tactics.constructor_tac false None i c in
- Tacticals.New.tclWITHHOLES false tac sigma bl
+ Proofview.V82.tclEVARS sigma <*> tac bl
]
END
@@ -138,7 +140,7 @@ TACTIC EXTEND specialize
[ "specialize" constr_with_bindings(c) ] -> [
let { Evd.sigma = sigma; it = c } = c in
let specialize c = Proofview.V82.tactic (Tactics.specialize c) in
- Tacticals.New.tclWITHHOLES false specialize sigma c
+ Proofview.V82.tclEVARS sigma <*> specialize c
]
END
@@ -159,7 +161,7 @@ END
TACTIC EXTEND split_with
[ "split" "with" bindings(bl) ] -> [
let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false) sigma [bl]
+ Proofview.V82.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
]
END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ec120f9c6..efe9dde78 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
open Evd
open Equality
open Misctypes
+open Proofview.Notations
DECLARE PLUGIN "extratactics"
@@ -32,17 +33,14 @@ TACTIC EXTEND admit
[ "admit" ] -> [ admit_as_an_axiom ]
END
-let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac =
- Tacticals.New.tclWITHHOLES false
+let replace_in_clause_maybe_by (sigma,c1) c2 cl tac =
+ Proofview.V82.tclEVARS sigma <*>
(replace_in_clause_maybe_by c1 c2 cl)
- sigma1
(Option.map Tacinterp.eval_tactic tac)
let replace_term dir_opt (sigma,c) cl =
- Tacticals.New.tclWITHHOLES false
- (replace_term dir_opt c)
- sigma
- cl
+ Proofview.V82.tclEVARS sigma <*>
+ (replace_term dir_opt c) cl
TACTIC EXTEND replace
["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -204,7 +202,7 @@ END
let onSomeWithHoles tac = function
| None -> tac None
- | Some c -> Tacticals.New.tclWITHHOLES false tac c.sigma (Some c.it)
+ | Some c -> Proofview.V82.tclEVARS c.sigma <*> tac (Some c.it)
TACTIC EXTEND contradiction
[ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -248,8 +246,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
- Tacticals.New. tclWITHHOLES false
- (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true
+ Proofview.V82.tclEVARS sigma <*>
+ general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true
TACTIC EXTEND rewrite_star
| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index df3115265..afd08026e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1716,7 +1716,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
- Tacticals.New.tclWITHHOLES false Tactics.intros_patterns sigma l'
+ Proofview.V82.tclEVARS sigma <*> Tactics.intros_patterns l'
end
| TacIntroMove (ido,hto) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -1808,7 +1808,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
let tac = Option.map (interp_tactic ist) t in
- Tacticals.New.tclWITHHOLES false (Tactics.forward b tac ipat) sigma c
+ Proofview.V82.tclEVARS sigma <*> Tactics.forward b tac ipat c
end
| TacGeneralize cl ->
let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
@@ -1816,7 +1816,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
- Tacticals.New.tclWITHHOLES false tac sigma cl
+ Proofview.V82.tclEVARS sigma <*> tac cl
end
| TacGeneralizeDep c ->
(new_interp_constr ist c)
@@ -1838,9 +1838,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
let with_eq = if b then None else Some (true,id) in
Tactics.letin_tac with_eq na c None cl
in
- Tacticals.New.tclWITHHOLES false
- (let_tac b (interp_fresh_name ist env na) c_interp clp)
- sigma eqpat
+ Proofview.V82.tclEVARS sigma <*>
+ let_tac b (interp_fresh_name ist env na) c_interp clp eqpat
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
@@ -1848,9 +1847,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
let with_eq = if b then None else Some (true,id) in
Tactics.letin_pat_tac with_eq na c cl
in
- Tacticals.New.tclWITHHOLES false
- (let_pat_tac b (interp_fresh_name ist env na)
- (interp_pure_open_constr ist env sigma c) clp) sigma eqpat
+ let_pat_tac b (interp_fresh_name ist env na)
+ (interp_pure_open_constr ist env sigma c) clp eqpat
end
(* Automation tactics *)
@@ -2024,7 +2022,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in
- Tacticals.New.tclWITHHOLES false (Inv.dinv k c_interp ids) sigma dqhyps
+ Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps
end
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -2033,8 +2031,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let hyps = interp_hyp_list ist env idl in
let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in
- Tacticals.New.tclWITHHOLES false (Inv.inv_clause k ids hyps)
- sigma dqhyps
+ Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps
end
| TacInversion (InversionUsing (c,idl),hyp) ->
Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e6e960a6..5123aed9c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1807,12 +1807,11 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma,c = f env sigma in
- Tacticals.New.tclWITHHOLES false
+ Proofview.V82.tclEVARS sigma <*>
(Tacticals.New.tclTHENFIRST
(* Skip the side conditions of the apply *)
(apply_in_once false true true true (Some (clear,naming)) id
(None,(sigma,(c,NoBindings))) tac_ipat))
- sigma
(tac thin None [])
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 10:22:25 +0000