- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,_,_ =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in