proof_status: proof_status; (** logical status *)
options: options;
objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
+ coercions: UriManager.uri list; (** defined coercions *)
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}