diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 | ||||
| -rw-r--r-- | plugins/fourier/fourierR.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 8 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
5 files changed, 10 insertions, 10 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 6abf96dcee..57268a9cfa 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -247,7 +247,7 @@ module Btauto = struct let fr = reify env fr in let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (Tactics.change_concl changed_gl); + Tactics.change_concl changed_gl; Tactics.apply (Lazy.force soundness); Proofview.V82.tactic (Tactics.normalise_vm_in_concl); try_unification env diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 551b210d37..4b70201b22 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -588,9 +588,9 @@ let rec fourier () = else tac_zero_infeq_false gl (rational_to_fraction cres) in tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl + [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] - ))) + )) (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) (Tacticals.New.tclTHENS (Equality.replace diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fd54584bc8..a38764c5bd 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -673,9 +673,9 @@ let mkDestructEq : tclTHENLIST [Simple.generalize new_hyps; (fun g2 -> - change_in_concl None + Proofview.V82.of_tactic (change_in_concl None (fun sigma -> - pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2); + pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert 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 diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 1835b6cc99..f9219407e9 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1282,7 +1282,7 @@ let resolution env full_reified_goal systems_list = Tactics.generalize (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> - Tactics.change_concl reified >> + Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> Tactics.normalise_vm_in_concl >> |