Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.

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 >>