let curi,metasenv,pbo,pty = proof in
let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let string_of_name =
let curi,metasenv,pbo,pty = proof in
let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let string_of_name =