diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:41:55 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:16:36 +0200 |
commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
tree | dd9e7016271fdad02452aed0f8cd469305e0780e /plugins/firstorder | |
parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'plugins/firstorder')
-rw-r--r-- | plugins/firstorder/instances.ml | 8 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 0e2a40245..5eff2f277 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -135,9 +135,9 @@ let left_instance_tac (inst,id) continue seq= [tclTHENLIST [Proofview.V82.of_tactic introf; pf_constr_of_global id (fun idc -> - (fun gls->generalize + (fun gls-> Proofview.V82.of_tactic (generalize [mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls)); + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -158,10 +158,10 @@ let left_instance_tac (inst,id) continue seq= try Typing.type_of (pf_env gl) evmap gt with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in - tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) + tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else pf_constr_of_global id (fun idc -> - generalize [mkApp(idc,[|t|])]) + Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) in tclTHENLIST [special_generalize; diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index d05e9484a..92b6e828e 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq= tclTHENLIST [pf_constr_of_global (find_left a seq) (fun left -> pf_constr_of_global id (fun id -> - generalize [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")) @@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [pf_constr_of_global id (fun idc -> generalize (newhyps idc)); + [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); clear_global id; tclDO lp (Proofview.V82.of_tactic intro)]) (wrap lp false continue seq) backtrack gl @@ -153,7 +153,7 @@ let ll_arrow_tac a b c backtrack id continue seq= 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 -> generalize [d idc]); + [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); clear_global id; Proofview.V82.of_tactic introf; Proofview.V82.of_tactic introf; @@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq= (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls)); + tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; |