(PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
in
assert (List.length goals = 0) ;
- let goals = List.map (fun (i,_,_) -> i) metasenv' in
let goals =
- List.filter
- (fun i ->
- not (List.exists (fun (j,_,_) -> i=j) metasenv)) goals
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+ ~newmetasenv:metasenv'
in
(proof',goals)
in