aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/coq_micromega.ml8
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