(Tacticals.then_
~start:
(ReductionTactics.fold_tac ~reduction:CicReduction.whd
- ~pattern:([],None)
- ~term:
- (Cic.Appl
- [_Rle ; _R0 ;
- Cic.Appl
- [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
- ]
- )
+ ~pattern:
+ (ProofEngineTypes.conclusion_pattern
+ (Some
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ )))
)
~continuation:
(Tacticals.then_
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
- ~with_what:(Cic.Appl [ _not; ineq]))
+ (PrimitiveTactics.change_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+ (Cic.Appl [ _not; ineq]))
status))
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
- ~with_what:w1) status in
+ (PrimitiveTactics.change_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+ w1) status
+ in
debug("fine MY_CHNGE\n");
r))
~continuation:(*PORTINGTacticals.id_tac*)tac2]))