| _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
in
ProofEngineTypes.apply_tactic
- (P.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
(C.Appl [
C.Lambda (
ProofEngineTypes.apply_tactic
(T.then_
~start:
- (P.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
(C.Appl [
C.Lambda (