aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/coretactics.ml431
-rw-r--r--tactics/extratactics.ml410
-rw-r--r--tactics/extratactics.mli2
-rw-r--r--tactics/tacinterp.ml16
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tacticals.mli1
6 files changed, 35 insertions, 33 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 2682ca0708..10de3e866a 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -74,15 +74,13 @@ 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 bl) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
]
END
TACTIC EXTEND eleft_with
[ "eleft" "with" bindings(bl) ] -> [
- let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true bl) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
]
END
@@ -98,15 +96,13 @@ 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 bl) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
]
END
TACTIC EXTEND eright_with
[ "eright" "with" bindings(bl) ] -> [
- let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true bl) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
]
END
@@ -118,9 +114,8 @@ TACTIC EXTEND constructor
Tactics.constructor_tac false None i NoBindings
]
| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
- let { Evd.sigma = sigma; it = bl } = bl in
- let tac = Tactics.constructor_tac false None i bl in
- Tacticals.New.tclWITHHOLES false tac sigma
+ let tac bl = Tactics.constructor_tac false None i bl in
+ Tacticals.New.tclDELAYEDWITHHOLES false bl tac
]
END
@@ -130,9 +125,8 @@ TACTIC EXTEND econstructor
Tactics.constructor_tac true None i NoBindings
]
| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
- let { Evd.sigma = sigma; it = bl } = bl in
- let tac = Tactics.constructor_tac true None i bl in
- Tacticals.New.tclWITHHOLES true tac sigma
+ let tac bl = Tactics.constructor_tac true None i bl in
+ Tacticals.New.tclDELAYEDWITHHOLES true bl tac
]
END
@@ -140,8 +134,7 @@ END
TACTIC EXTEND specialize
[ "specialize" constr_with_bindings(c) ] -> [
- let { Evd.sigma = sigma; it = c } = c in
- Tacticals.New.tclWITHHOLES false (Tactics.specialize c) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize
]
END
@@ -161,15 +154,13 @@ 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 [bl]) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
]
END
TACTIC EXTEND esplit_with
[ "esplit" "with" bindings(bl) ] -> [
- let { Evd.sigma = sigma ; it = bl } = bl in
- Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true [bl]) sigma
+ Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
]
END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4ddf9c1162..dce7a18608 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -70,8 +70,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 (Some (None,ElimOnConstr c.it))) c.sigma
+ Tacticals.New.tclDELAYEDWITHHOLES with_evars c
+ (fun c -> tac with_evars (Some (None,ElimOnConstr c)))
TACTIC EXTEND simplify_eq_main
| [ "simplify_eq" constr_with_bindings(c) ] ->
@@ -116,7 +116,7 @@ END
open Proofview.Notations
let discrHyp id =
Proofview.tclEVARMAP >>= fun sigma ->
- discr_main {it = Term.mkVar id,NoBindings; sigma = sigma;}
+ discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
let injection_main c =
elimOnConstrWithHoles (injClause None) false c
@@ -161,7 +161,7 @@ END
let injHyp id =
Proofview.tclEVARMAP >>= fun sigma ->
- injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
+ injection_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -201,7 +201,7 @@ END
let onSomeWithHoles tac = function
| None -> tac None
- | Some c -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma
+ | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
TACTIC EXTEND contradiction
[ "contradiction" constr_with_bindings_opt(c) ] ->
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 72c2679c06..1d2e497d51 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,4 +11,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic
(* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
-val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic
+val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d96c8f98a2..16cafafeb8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2277,13 +2277,15 @@ let () =
let lift f = (); fun ist gl x -> (project gl, f ist (pf_env gl) (project gl) x)
let lifts f = (); fun ist gl x -> f ist (pf_env gl) (project gl) x
-let interp_bindings' ist gl bl =
- let (sigma, bl) = interp_bindings ist (pf_env gl) (project gl) bl in
- (project gl, pack_sigma (sigma, bl))
-
-let interp_constr_with_bindings' ist gl c =
- let (sigma, c) = interp_constr_with_bindings ist (pf_env gl) (project gl) c in
- (project gl, pack_sigma (sigma, c))
+let interp_bindings' ist gl bl = (project gl, { delayed = fun env sigma ->
+ let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in
+ Sigma.Unsafe.of_pair (bl, sigma)
+ })
+
+let interp_constr_with_bindings' ist gl c = (project gl, { delayed = fun env sigma ->
+ let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
+ Sigma.Unsafe.of_pair (c, sigma)
+ })
let () =
Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n);
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e181c8e14e..74714300c4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -515,6 +515,14 @@ module New = struct
in
Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
+ let tclDELAYEDWITHHOLES check x tac =
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let Sigma (x, sigma, _) = x.Tacexpr.delayed env sigma in
+ tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
+ end }
+
let tclTIMEOUT n t =
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 80e01a8d07..042f80fe82 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -219,6 +219,7 @@ module New : sig
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
+ val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
val tclTIMEOUT : int -> unit tactic -> unit tactic
val tclTIME : string option -> 'a tactic -> 'a tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-11 21:16:44 +0000