diff options
Diffstat (limited to 'plugins/firstorder/rules.ml')
| -rw-r--r-- | plugins/firstorder/rules.ml | 9 |
1 files changed, 5 insertions, 4 deletions
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)]) |