apply_tactic
(Tacticals.then_
~start:
- (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+ (ReductionTactics.fold_tac
+ ~reduction:(const_lazy_reduction CicReduction.whd)
~pattern:(ProofEngineTypes.conclusion_pattern None)
~term:
- (Cic.Appl
+ (const_lazy_term
+ (Cic.Appl
[_Rle ; _R0 ;
Cic.Appl
- [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))
+ [_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))))
+ ~continuation:(tac_zero_inf_pos (-n,d))))
status
in
mk_tactic (tac_zero_infeq_false gl (n,d))
let tcl_fail a (proof,goal) =
match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
| _ -> (proof,[goal])
;;
apply_tactic
(ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
- (Cic.Appl [ _not; ineq]))
+ (const_lazy_term (Cic.Appl [ _not; ineq])))
status))
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
let r = apply_tactic
(ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
- w1) status
+ (const_lazy_term w1)) status
in
debug("fine MY_CHNGE\n");
r))