options: options;
objects: UriManager.uri list;
coercions: UriManager.uri list;
+ universe:Universe.universe;
}
let get_current_proof status =
match status.proof_status with
| Incomplete_proof { proof = p } -> p
+ | Proof p -> p
| _ -> raise (Statement_error "no ongoing proof")
let get_proof_metasenv status =