Moving conversion functions to the new tactic API.

3 files changed, 14 insertions, 14 deletions

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