aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/cc/cctac.ml6
-rw-r--r--plugins/firstorder/rules.ml9
-rw-r--r--plugins/fourier/fourierR.ml4
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/tacticals.ml14
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml6
7 files changed, 23 insertions, 24 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2d9dec095..b2c609dcb 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -245,7 +245,7 @@ let app_global f args k =
Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
let new_app_global f args k =
- Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+ Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
let new_refine c = Proofview.V82.tactic (refine c)
let refine c = refine c
@@ -492,7 +492,7 @@ let congruence_tac depth l =
*)
let mk_eq f c1 c2 k =
- Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+ Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
Proofview.Goal.enter { enter = begin fun gl ->
let open Tacmach.New in
let evm, ty = pf_apply type_of gl c1 in
@@ -501,7 +501,7 @@ let mk_eq f c1 c2 k =
let evm, _ = type_of (pf_env gl) evm term in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
(k term)
- end })
+ end }
let f_equal =
Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a60fd4d8f..96601f74a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -14,6 +14,7 @@ open Vars
open Tacmach
open Tactics
open Tacticals
+open Proofview.Notations
open Termops
open Formula
open Sequent
@@ -96,7 +97,7 @@ let left_and_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
(tclTHENLIST
- [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
+ [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim);
clear_global id;
tclDO n (Proofview.V82.of_tactic intro)])
(wrap n false continue seq)
@@ -110,12 +111,12 @@ let left_or_tac ind backtrack id continue seq gls=
tclDO n (Proofview.V82.of_tactic intro);
wrap n false continue seq] in
tclIFTHENSVELSE
- (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
(Array.map f v)
backtrack gls
let left_false_tac id=
- Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
+ Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
(* left arrow connective rules *)
@@ -183,7 +184,7 @@ let forall_tac backtrack continue seq=
let left_exists_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
- (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
(tclTHENLIST [clear_global id;
tclDO n (Proofview.V82.of_tactic intro);
(wrap (n-1) false continue seq)])
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index e11cbc279..25d8f8c83 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -617,9 +617,9 @@ let rec fourier () =
[Tacticals.New.tclORELSE
(* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
(Proofview.tclUNIT ());
- Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
+ Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq ->
(Tacticals.New.tclTHEN (apply symeq)
- (apply (get coq_Rinv_1))))]
+ (apply (get coq_Rinv_1)))]
)
]));
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e68be91e9..25c28cf4a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -658,8 +658,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| Some evd ->
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
- Tacticals.New.pf_constr_of_global sym (fun sym ->
- Tacticals.New.pf_constr_of_global e (fun e ->
+ Tacticals.New.pf_constr_of_global sym >>= fun sym ->
+ Tacticals.New.pf_constr_of_global e >>= fun e ->
let eq = applist (e, [t1;c1;c2]) in
tclTHENLAST
(replace_core clause l2r eq)
@@ -667,7 +667,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
[assumption;
tclTHEN (apply sym) assumption;
try_prove_eq
- ])))
+ ])
end }
let replace c1 c2 =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5c97f27ba..c8441a8cc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -732,13 +732,11 @@ module New = struct
let case_nodep_then_using =
general_elim_then_using gl_make_case_nodep false
- let pf_constr_of_global ref tac =
- Proofview.Goal.enter { enter = begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let (sigma, c) = Evd.fresh_global env sigma ref in
- let c = EConstr.of_constr c in
- Proofview.Unsafe.tclEVARS sigma <*> (tac c)
- end }
+ let pf_constr_of_global ref =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.tclENV >>= fun env ->
+ let (sigma, c) = Evd.fresh_global env sigma ref in
+ let c = EConstr.of_constr c in
+ Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 01b9e5e93..5a4ecbac7 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -263,5 +263,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+ val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1615aec89..9c2a1d850 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4721,7 +4721,7 @@ let symmetry_red allowred =
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
(convert_concl_no_check concl DEFAULTcast)
- (Tacticals.New.pf_constr_of_global eq_data.sym apply)
+ (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
end }
@@ -4817,8 +4817,8 @@ let transitivity_red allowred t =
Tacticals.New.tclTHEN
(convert_concl_no_check concl DEFAULTcast)
(match t with
- | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
- | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+ | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+ | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
| None,eq,eq_kind ->
match t with
| None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:52:58 +0000