(* 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. *)
-(* REMOVE
-module StringMap = Map.Make (String)
-type option_value =
- | String of string
- | Int of int
-*)
-(* type options = option_value StringMap.t *)
-(* let no_options = StringMap.empty *)
-
type status = {
moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status;
-(* options: options; *)
objects: UriManager.uri list;
- coercions: UriManager.uri list;
+ coercions: CoercDb.coerc_db;
universe:Universe.universe;
baseuri: string;
}