-let tac_zero_infeq_false gl (n,d) ~status=
-debug("stat tac_zero_infeq_false");
-let r =
- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+debug("stat tac_zero_infeq_false\n");
+(*let r =
+ (
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+ Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)