;;
let apply_tactic ~tactic =
+ let module PET = ProofEngineTypes in
match get_proof (),!goal with
| None,_
| _,None -> assert false
| Some proof', Some goal' ->
- let (newproof, newgoals) = tactic (proof', goal') in
+ let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in
set_proof (Some newproof);
goal :=
(match newgoals, newproof with