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/micromega | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |