From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:41:55 +0200 Subject: Put the "generalize" tactic in the monad. --- plugins/firstorder/instances.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder/instances.ml') 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; -- cgit v1.2.3