- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
- ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
- debug("stat tac_zero_infeq_false");
- r
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("faccio fold di " ^ CicPp.ppterm
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ ) ^ "\n") ;
+ debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+ (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
+ Tacticals.then_
+ ~start:
+ (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+ ~also_in_hypotheses:false
+ ~term:
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ )
+ )
+ ~continuation:
+ (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+ ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
+ debug("end tac_zero_infeq_false\n");
+ r
+(*PORTING
+ Tacticals.id_tac ~status
+*)