Tacticals.then_
~start:(Tactics.change
~pattern:(ProofEngineTypes.conclusion_pattern None)
- (fun _ metasenv ugraph -> ty',metasenv,ugraph))
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph))
~continuation:just
)
| Some id ->
match just with
None ->
Tactics.auto ~dbd
- ~params:["paramodulation","1"; "timeout","3"]
+ ~params:["paramodulation","1"; "timeout","3"; "library","1"]
| Some just -> Tactics.apply just
in
match lhs with