- (ReductionTactics.fold_tac ~reduction:CicReduction.whd
- ~pattern:
- (ProofEngineTypes.conclusion_pattern
- (Some
- (Cic.Appl
- [_Rle ; _R0 ;
- Cic.Appl
- [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
- ]
- )))
- )
+ (ReductionTactics.fold_tac
+ ~reduction:(const_lazy_reduction CicReduction.whd)
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ ~term:
+ (const_lazy_term
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))