(* Status in which the proof could be while it is being processed by the
* engine. No status entering/exiting the engine could be in it. *)
(* Status in which the proof could be while it is being processed by the
* engine. No status entering/exiting the engine could be in it. *)
objects: UriManager.uri list;
coercions: UriManager.uri list;
universe:Universe.universe;
objects: UriManager.uri list;
coercions: UriManager.uri list;
universe:Universe.universe;
let get_option status name =
try
StringMap.find name status.options
with Not_found -> raise (Option_error (name, "not found"))
let get_option status name =
try
StringMap.find name status.options
with Not_found -> raise (Option_error (name, "not found"))
match get_option status name with
| String s -> s
| _ -> raise (Option_error (name, "not a string value"))
match get_option status name with
| String s -> s
| _ -> raise (Option_error (name, "not a string value"))