diff options
| author | Hugo Herbelin | 2014-12-07 18:32:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-07 18:39:31 +0100 |
| commit | 2fa05a8d300f5c0d375a558a8bced972eea4bfaf (patch) | |
| tree | ecc7fa89b5f4be1bcc045fcd0d75e2b20f289566 /plugins/micromega | |
| parent | 2acc6327e4d8a05898b75cb3abb47b7941ec420a (diff) | |
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
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 db22727fc4..dfeeb49047 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1392,7 +1392,7 @@ let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = (* todo : directly generate the proof term - or generalize befor conversion? *) Tacticals.tclTHENSEQ [ (fun gl -> - Tactics.change_concl + Proofview.V82.of_tactic (Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); @@ -1401,7 +1401,7 @@ let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl)) gl); + (Tacmach.pf_concl gl))) gl); Tactics.generalize env ; Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; ] @@ -1683,7 +1683,7 @@ let micromega_order_changer cert env ff gl = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Tactics.change_concl + Proofview.V82.of_tactic (Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); @@ -1693,7 +1693,7 @@ let micromega_order_changer cert env ff gl = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl) - ) + )) gl |