-(*
- let tac1=ref (if h1.hstrict
- then (tclTHENS (apply (parse "Rfourier_lt"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])
- else (tclTHENS (apply (parse "Rfourier_le"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])) in
- s:=h1.hstrict;
- List.iter (fun (h,c)->
- (if (!s)
- then (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)]))
- else (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])));
- s:=(!s)||(h.hstrict))
- lutil;
- let tac2= if sres
- then tac_zero_inf_false gl (rational_to_fraction cres)
- else tac_zero_infeq_false gl (rational_to_fraction cres)
+ debug "inizio a costruire tac1\n";
+ let tac1=ref ( if h1.hstrict then
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
+ ~continuations:[tac_use h1;tac_zero_inf_pos goal
+ (rational_to_fraction c1)])
+ else
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
+ ~continuations:[tac_use h1;tac_zero_inf_pos goal
+ (rational_to_fraction c1)]))
+ in
+ s:=h1.hstrict;
+
+ List.iter (fun (h,c) ->
+ (if (!s) then
+ (if h.hstrict then
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_lt)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ else
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_le)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ )
+ else
+ (if h.hstrict then
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ else
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])));
+ s:=(!s)||(h.hstrict))
+ lutil;(*end List.iter*)
+
+ let tac2= if sres then
+ tac_zero_inf_false goal (rational_to_fraction cres)
+ else
+ tac_zero_infeq_false goal (rational_to_fraction cres)