Moving conversion functions to the new tactic API.

8 files changed, 43 insertions, 43 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 5a49fc8f4..57eb80f5f 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -250,7 +250,7 @@ module Btauto = struct
           Tacticals.New.tclTHENLIST [
             Tactics.change_concl changed_gl;
             Tactics.apply (Lazy.force soundness);
-            Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+            Tactics.normalise_vm_in_concl;
             try_unification env
           ]
       | _ ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e676a8a93..d539eda57 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -210,6 +210,6 @@ let defined_connectives=lazy
 let normalize_evaluables=
   onAllHypsAndConcl
     (function
-	 None->unfold_in_concl (Lazy.force defined_connectives)
+	 None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
        | Some id ->
-	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+	   Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4eab5f912..aa89f89b7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1334,7 +1334,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		 in
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
-		   [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
+		   [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
 		    let do_prove =
 		      build_proof
 			interactive_proof
@@ -1460,7 +1460,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 		  (fun g ->
 		     if is_mes
 		     then
-		       unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+		       Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g
 		     else tclIDTAC g
 		  );
 		  observe_tac "rew_and_finish"
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0c9d3bb81..ae2091a22 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -484,15 +484,15 @@ and intros_with_rewrite_aux : tactic =
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
-			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
-			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
 		      else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) 
 		      then tclTHENSEQ[
-			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))];
-			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
@@ -703,7 +703,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  thin ids
 	]
       else
-        unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
+        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))])
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b09678341..834d0acea 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -276,8 +276,8 @@ let tclUSER tac is_mes l g =
       if is_mes
       then observe_tclTHENLIST (str "tclUSER2")
         [
-	  unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
-            (delayed_force Indfun_common.ltof_ref))];
+	  Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+            (delayed_force Indfun_common.ltof_ref))]);
          tac
 	 ]
       else tac
@@ -564,8 +564,8 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 		     h_intros [k;h';def];
 		     observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
 		     observe_tac (str "unfold functional")
-		       (unfold_in_concl[(Locus.OnlyOccurrences [1],
-					 evaluable_of_global_reference infos.func)]);
+		       (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+					 evaluable_of_global_reference infos.func)]));
 		     (
 		       observe_tclTHENLIST (str "test")[
 			 list_rewrite true
@@ -904,8 +904,8 @@ let make_rewrite expr_info l hp max =
 	 (observe_tclTHENLIST (str "make_rewrite")[
 	   simpl_iter Locusops.onConcl;
 	   observe_tac (str "unfold functional")
-	     (unfold_in_concl[(Locus.OnlyOccurrences [1],
-			       evaluable_of_global_reference expr_info.func)]);
+	     (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+			       evaluable_of_global_reference expr_info.func)]));
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
@@ -1425,7 +1425,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   let x = n_x_id ids nargs in
   observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
     h_intros x;
-    unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
+    Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
     observe_tac (str "simplest_case")
       (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x)))));
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 7e38109d6..ad63c90f2 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -927,15 +927,15 @@ let rec transform p t =
 	  transform p
 	    (mkApp (Lazy.force coq_Zplus,
 		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
-	unfold sp_Zminus :: tac,t
+	Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
     | Kapp(Zsucc,[t1]) ->
 	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer one |])) in
-	unfold sp_Zsucc :: tac,t
+	Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
     | Kapp(Zpred,[t1]) ->
 	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer negone |])) in
-	unfold sp_Zpred :: tac,t
+	Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
    | Kapp(Zmult,[t1;t2]) ->
        let tac1,t1' = transform (P_APP 1 :: p) t1
        and tac2,t2' = transform (P_APP 2 :: p) t2 in
@@ -1091,8 +1091,8 @@ let replay_history tactic_normalisation =
 	    in
             Tacticals.New.tclTHENS
 	      (Tacticals.New.tclTHENLIST [
-		Proofview.V82.tactic (unfold sp_Zle);
-		Proofview.V82.tactic (simpl_in_concl);
+		unfold sp_Zle;
+		simpl_in_concl;
 		intro;
 		(absurd not_sup_sup) ])
 	      [ assumption ; reflexivity ]
@@ -1135,10 +1135,10 @@ let replay_history tactic_normalisation =
 		        (intros_using [id]);
 		        (loop l) ];
 		      Tacticals.New.tclTHENLIST [
-			(Proofview.V82.tactic (unfold sp_Zgt));
-			(Proofview.V82.tactic simpl_in_concl);
+			(unfold sp_Zgt);
+			simpl_in_concl;
 			reflexivity ] ];
-		  Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ]
+		  Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
                 ];
 	      Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
 
@@ -1160,18 +1160,18 @@ let replay_history tactic_normalisation =
 		    [mkApp (Lazy.force coq_OMEGA4,
                       [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
 		  Proofview.V82.tactic (clear [aux1;aux2]);
-		  Proofview.V82.tactic (unfold sp_not);
+		  unfold sp_not;
 		  (intros_using [aux]);
 		  Proofview.V82.tactic (resolve_id aux);
 		  Proofview.V82.tactic (mk_then tac);
 		  assumption ] ;
 		 Tacticals.New.tclTHENLIST [
-		   Proofview.V82.tactic (unfold sp_Zgt);
-		   Proofview.V82.tactic simpl_in_concl;
+		   unfold sp_Zgt;
+		   simpl_in_concl;
 		   reflexivity ] ];
               Tacticals.New.tclTHENLIST [
-		Proofview.V82.tactic (unfold sp_Zgt);
-                Proofview.V82.tactic simpl_in_concl;
+		unfold sp_Zgt;
+                simpl_in_concl;
 		reflexivity ] ]
       | EXACT_DIVIDE (e1,k) :: l ->
 	  let id = hyp_of_tag e1.id in
@@ -1208,8 +1208,8 @@ let replay_history tactic_normalisation =
 		   (intros_using [id]);
 		   (loop l) ];
 		  Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (unfold sp_Zgt);
-                    Proofview.V82.tactic simpl_in_concl;
+		    unfold sp_Zgt;
+                    simpl_in_concl;
 		    reflexivity ] ];
 		Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
       | (MERGE_EQ(e3,e1,e2)) :: l ->
@@ -1329,12 +1329,12 @@ let replay_history tactic_normalisation =
 		   (intros_using [id]);
 		   (loop l) ];
 		 Tacticals.New.tclTHENLIST [
-		   Proofview.V82.tactic (unfold sp_Zgt);
-                   Proofview.V82.tactic simpl_in_concl;
+		   unfold sp_Zgt;
+                   simpl_in_concl;
 		   reflexivity ] ];
 	      Tacticals.New.tclTHENLIST [
-		Proofview.V82.tactic (unfold sp_Zgt);
-                Proofview.V82.tactic simpl_in_concl;
+		unfold sp_Zgt;
+                simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
 	  Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
@@ -1343,9 +1343,9 @@ let replay_history tactic_normalisation =
       | CONSTANT_NEG(e,k) :: l ->
 	  Tacticals.New.tclTHENLIST [
 	    Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
-            Proofview.V82.tactic (unfold sp_Zle);
-	    Proofview.V82.tactic simpl_in_concl;
-	    Proofview.V82.tactic (unfold sp_not);
+            unfold sp_Zle;
+	    simpl_in_concl;
+	    unfold sp_not;
 	    (intros_using [aux]);
 	    Proofview.V82.tactic (resolve_id aux);
 	    reflexivity
@@ -1839,7 +1839,7 @@ let destructure_goal =
       match destructurate_prop t with
       | Kapp(Not,[t]) ->
           (Tacticals.New.tclTHEN
-	     (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro)
+	     (Tacticals.New.tclTHEN (unfold sp_not) intro)
 	     destructure_hyps)
       | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 560e6a899..177c870b3 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list =
   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 >>
+  Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
   (*i Alternatives to the previous line:
    - Normalisation without VM:
       Tactics.normalise_in_concl
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index ed6db90d6..a67cc7cb8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -99,10 +99,10 @@ let protect_red map env sigma c =
     (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
 
 let protect_tac map =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
+  Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
+  Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));;
 
 
 (****************************************************************************)