More conversion functions in the new tactic API.

9 files changed, 42 insertions, 40 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index aa89f89b74..86302dc6ce 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 d1e1098259..41fd0bd18e 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 ae2091a227..2b45206bb4 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 834d0aceac..6c6caa6284 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)]));
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6caebf6c4f..1d6cd8e99b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -390,7 +390,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Unfold_nth c ->
       Proofview.V82.tactic (fun gl ->
        if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
+	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
        else tclFAIL 0 (str"Unbound reference") gl)
     | Extern tacast -> 
       conclPattern concl p tacast
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ae85f02d59..f2d26ec86b 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -198,7 +198,7 @@ and e_my_find_search db_list local_db hdc concl =
         | Res_pf_THEN_trivial_fail (term,cl) ->
           Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
             (e_trivial_fail_db db_list local_db)
-        | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
+        | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
         | Extern tacast -> conclPattern concl p tacast
        in
        let tac = run_hint t tac in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 91711c2f74..73aa4c3373 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1967,7 +1967,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
         tclTHEN
 	  (tclEVARS sigma)
-	  (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
+	  (Proofview.V82.of_tactic (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)))
           gl
       end
       end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28d3ed18a1..210888b67c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -569,8 +569,8 @@ let reduct_option ?(check=false) redfun = function
 (** Tactic reduction modulo evars (for universes essentially) *)
 
 let pf_e_reduce_decl redfun where (id,c,ty) gl =
-  let sigma = project gl in
-  let redfun = redfun (pf_env gl) in
+  let sigma = Tacmach.New.project gl in
+  let redfun = redfun (Tacmach.New.pf_env gl) in
   match c with
   | None ->
       if where == InHypValueOnly then
@@ -582,17 +582,17 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl =
       let sigma, ty' = if where != InHypValueOnly then redfun sigma ty else sigma, ty in
 	sigma, (id,Some b',ty')
 
-let e_reduct_in_concl (redfun,sty) gl =
-  Proofview.V82.of_tactic
-    (let sigma, c' = (Tacmach.pf_apply redfun gl (Tacmach.pf_concl gl)) in
-       Proofview.Unsafe.tclEVARS sigma <*> 
-	 convert_concl_no_check c' sty) gl
+let e_reduct_in_concl (redfun, sty) =
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma, c' = Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl) in
+    Sigma.Unsafe.of_pair (convert_concl_no_check c' sty, sigma)
+  end }
 
-let e_reduct_in_hyp ?(check=false) redfun (id,where) gl =
-  Proofview.V82.of_tactic 
-    (let sigma, decl' = pf_e_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl in
-       Proofview.Unsafe.tclEVARS sigma <*> 
-	 convert_hyp ~check decl') gl
+let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+    let sigma, decl' = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+    Sigma.Unsafe.of_pair (convert_hyp ~check decl', sigma)
+  end }
 
 let e_reduct_option ?(check=false) redfun = function
   | Some id -> e_reduct_in_hyp ~check (fst redfun) id
@@ -739,14 +739,16 @@ let reduction_clause redexp cl =
     | OnConcl occs ->
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
-let reduce redexp cl goal =
-  let cl = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps goal) cl in
+let reduce redexp cl =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
   let redexps = reduction_clause redexp cl in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
-  let tac = tclMAP (fun (where,redexp) ->
+  let tac = Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
-      (Redexpr.reduction_of_red_expr (Tacmach.pf_env goal) redexp) where) redexps in
-  if check then with_check tac goal else tac goal
+      (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps in
+  if check then Proofview.V82.tactic (fun gl -> with_check (Proofview.V82.of_tactic tac) gl) else tac (** FIXME *)
+  end }
 
 (* Unfolding occurrences of a constant *)
 
@@ -3943,7 +3945,7 @@ let induction_without_atomization isrec with_evars elim names lid =
     if indvars = [] then [List.hd lid_params] else indvars in
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
     (* pattern to make the predicate appear. *)
-    reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl;
+    Proofview.V82.of_tactic (reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl);
     (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all
        possible holes using arguments given by the user (but the
        functional one). *)
@@ -4717,9 +4719,9 @@ module New = struct
   open Locus
 
   let reduce_after_refine =
-    Proofview.V82.tactic (reduce
+    reduce
       (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences })
+      {onhyps=None; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Proofview.Refine.refine ?unsafe c <*>
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 657367e36c..367430d918 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -157,8 +157,8 @@ val unfold_option     :
 val change            :
   constr_pattern option -> change_arg -> clause -> tactic
 val pattern_option    :
-  (occurrences * constr) list -> goal_location -> tactic
-val reduce            : red_expr -> clause -> tactic
+  (occurrences * constr) list -> goal_location -> unit Proofview.tactic
+val reduce            : red_expr -> clause -> unit Proofview.tactic
 val unfold_constr     : global_reference -> unit Proofview.tactic
 
 (** {6 Modification of the local context. } *)