assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in