aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-04-11 14:27:24 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-04-24 17:59:21 +0200
commitd272cd02ef9ba2509c266f58ee39f51106ae53c2 (patch)
tree506223959f09e7c9f8f2b4d6ac6c4261daf9480a /tactics
parent1ef92c718ece547826f4c7e5c1ce78a6965e1ca6 (diff)
Fix the API of the new pf_constr_of_global.
The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/tacticals.ml14
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml6
4 files changed, 13 insertions, 15 deletions
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.")