More conversion functions in the new tactic API.

4 files changed, 15 insertions, 15 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index aa89f89b7..86302dc6c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -371,12 +371,12 @@ let isLetIn t =
     | _ -> false
 
 
-let h_reduce_with_zeta =
-  reduce
+let h_reduce_with_zeta cl =
+  Proofview.V82.of_tactic (reduce
     (Genredexpr.Cbv
        {Redops.all_flags
 	with Genredexpr.rDelta = false;
-       })
+       }) cl)
 
 
 
@@ -707,7 +707,7 @@ let build_proof
 		    [
 		      generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
-		      pattern_option [Locus.AllOccurrencesBut [1],t] None;
+		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d1e109825..41fd0bd18 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -113,7 +113,7 @@ let functional_induction with_clean c princl pat =
 	in
 	Tacticals.tclTHEN
 	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
-	  (Tactics.reduce flag Locusops.allHypsAndConcl)
+	  (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
 	  g
       else Tacticals.tclIDTAC g
     in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ae2091a22..2b45206bb 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -363,14 +363,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    (* unfolding of all the defined variables introduced by this branch *)
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
-	    reduce
+	    Proofview.V82.of_tactic (reduce
 	      (Genredexpr.Cbv
 		 { Redops.all_flags with
 		     Genredexpr.rDelta = false ;
 		     Genredexpr.rConst = []
 		 }
 	      )
-	      Locusops.onConcl;
+	      Locusops.onConcl);
 	    observe_tac ("toto ") tclIDTAC;
     
 	    (* introducing the the result of the graph and the equality hypothesis *)
@@ -532,12 +532,12 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		  | LetIn _ ->
 		      tclTHENSEQ[
-			reduce
+			Proofview.V82.of_tactic (reduce
 			  (Genredexpr.Cbv
 			     {Redops.all_flags
 			      with Genredexpr.rDelta = false;
 			     })
-			  Locusops.onConcl
+			  Locusops.onConcl)
 			;
 			intros_with_rewrite
 		      ] g
@@ -547,12 +547,12 @@ and intros_with_rewrite_aux : tactic =
 	      end
 	  | LetIn _ ->
 	      tclTHENSEQ[
-		reduce
+		Proofview.V82.of_tactic (reduce
 		  (Genredexpr.Cbv
 		     {Redops.all_flags
 		      with Genredexpr.rDelta = false;
 		     })
-		  Locusops.onConcl
+		  Locusops.onConcl)
 		;
 		intros_with_rewrite
 	      ] g
@@ -692,12 +692,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
-	  reduce
+	  Proofview.V82.of_tactic (reduce
 	    (Genredexpr.Cbv
 	       {Redops.all_flags
 		with Genredexpr.rDelta = false;
 	       })
-	    Locusops.onConcl
+	    Locusops.onConcl)
 	  ;
 	  generalize (List.map mkVar ids);
 	  thin ids
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 834d0acea..6c6caa628 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -562,7 +562,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
 		     observe_tac (str "clearing k ") (clear [id]);
 		     h_intros [k;h';def];
-		     observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
+		     observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
 		     observe_tac (str "unfold functional")
 		       (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
 					 evaluable_of_global_reference infos.func)]));
@@ -902,7 +902,7 @@ let make_rewrite expr_info l hp max =
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (observe_tclTHENLIST (str "make_rewrite")[
-	   simpl_iter Locusops.onConcl;
+	   Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
 	   observe_tac (str "unfold functional")
 	     (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
 			       evaluable_of_global_reference expr_info.func)]));