let initial_proof = (Some uri, metasenv, bo, ty) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv in
{ status with GrafiteTypes.proof_status =
let initial_proof = (Some uri, metasenv, bo, ty) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv in
{ status with GrafiteTypes.proof_status =