From d272cd02ef9ba2509c266f58ee39f51106ae53c2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Apr 2017 14:27:24 +0200 Subject: 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. --- plugins/firstorder/rules.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder') 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)]) -- cgit v1.2.3