let uri,metasenv,pbo,pty = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)
let uri,metasenv,pbo,pty = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)