From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:25:11 +0100 Subject: Removing compatibility layers from Tacticals --- plugins/firstorder/rules.ml | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 38dae0b20..36bd91ab6 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -59,16 +59,17 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))) + try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= + let open EConstr in tclIFTHENELSE (try tclTHENLIST [pf_constr_of_global (find_left a seq) (fun left -> pf_constr_of_global id (fun id -> - Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))]))); + Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))]))); clear_global id; Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) @@ -95,7 +96,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 (EConstr.of_constr %> 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) @@ -109,12 +110,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 (EConstr.of_constr %> 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 (EConstr.of_constr %> simplest_elim)) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) (* left arrow connective rules *) @@ -133,7 +134,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let head=mkApp ((lift p idc),[|capply|]) in EConstr.of_constr (it_mkLambda_or_LetIn head rc) in let lp=Array.length rcs in - let newhyps idc =List.init lp (myterm idc) in + let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in tclIFTHENELSE (tclTHENLIST [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); @@ -142,17 +143,22 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= (wrap lp false continue seq) backtrack gl let ll_arrow_tac a b c backtrack id continue seq= + let open EConstr in + let open Vars in + let a = EConstr.of_constr a in + let b = EConstr.of_constr b in + let c = EConstr.of_constr c in let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc =EConstr.of_constr (mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in + let d idc = mkLambda (Anonymous,b, + mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c))) + (tclTHENS (Proofview.V82.of_tactic (cut c)) [tclTHENLIST [Proofview.V82.of_tactic introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc))) - [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))); + tclTHENS (Proofview.V82.of_tactic (cut cc)) + [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); tclTHENLIST [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); clear_global id; @@ -177,7 +183,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 (EConstr.of_constr %> 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)]) @@ -191,9 +197,9 @@ let ll_forall_tac prod backtrack id continue seq= [Proofview.V82.of_tactic intro; pf_constr_of_global id (fun idc -> (fun gls-> + let open EConstr in let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - let term = EConstr.of_constr term in tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; -- cgit v1.2.3