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/micromega/coq_micromega.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 5c0a8226a..0fcfbfc71 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1464,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ] (Tacmach.pf_concl gl)) ; - Tactics.new_generalize env ; + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1726,7 +1726,7 @@ let micromega_gen | Some (ids,ff',res') -> (Tacticals.New.tclTHENLIST [ - Tactics.new_generalize (List.map Term.mkVar ids) ; + Tactics.generalize (List.map Term.mkVar ids) ; micromega_order_change spec res' (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' ]) @@ -1774,7 +1774,7 @@ let micromega_order_changer cert env ff = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl))); - Tactics.new_generalize env ; + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1812,7 +1812,7 @@ let micromega_genr prover = (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in (Tacticals.New.tclTHENLIST [ - Tactics.new_generalize (List.map Term.mkVar ids) ; + Tactics.generalize (List.map Term.mkVar ids) ; micromega_order_changer res' env (abstract_wrt_formula ff' ff) ]) with -- cgit v1.2.3