(Tacticals.then_
~start:
(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]]
- ]
- )))
- )
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ ~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)
)
context
in
- Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+ Tacticals.first ~tactics:tac_list (proof,goal)
;;
*)
(* Galla: moved in negationTactics.ml
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
(Cic.Appl [ _not; ineq]))
status))
r))
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1;
- Tacticals.try_tactics
+ Tacticals.first
~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
])
;(*Tacticals.id_tac*)
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
w1) status
in