ring.ml* splitted into ring.ml* and tacticals.ml*

[helm.git] / helm / gTopLevel / fourierR.ml

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index b8d88ae193b14902bfafa43b2f74a14000645fda..815a39aa1ba9b05675b523de0605f11d345ae2bd 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -461,24 +461,15 @@ let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_
 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
 
 
-let tcl_then ~start ~continuation ~status = 
-   let tcl_then_aux (proof,goals) goal =
-      let (newproof,newgoals) = continuation ~status:(proof,goal) in
-      (newproof, goals @ newgoals)
-   in
-   let (proof,new_goals) = start ~status in
-   List.fold_left tcl_then_aux (proof,[]) new_goals
-;;
-
 let tac_zero_inf_pos gl (n,d) =
    (*let cste = pf_parse_constr gl in*)
    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
    for i=1 to n-1 do 
-       tacn:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
+       tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
    for i=1 to d-1 do
-       tacd:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
-   (Ring.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
+       tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
+   (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
 ;;
 
 (* preuve que 0<=n*1/d