-(*let tac_zero_inf_pos gl (n,d) =
- let cste = pf_parse_constr gl in
- let tacn=ref (apply (cste "Rlt_zero_1")) in
- let tacd=ref (apply (cste "Rlt_zero_1")) in
+
+let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
+
+let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
+
+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