- (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
- ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)
+ (Tacticals.thens ~start:(
+ fun ~status ->
+ debug ("inizio t1 strict\n");
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
+ debug ("ty = "^ CicPp.ppterm ty^"\n");
+
+ PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
+ ~continuations:[tac_use h1;
+
+ Ring.id_tac] ~status
+
+ (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
+
+ )