+type item =
+ [ `Obj of NUri.uri * NCic.obj
+ | `Constr of NCic.universe * NCic.universe ]
+;;
+
+type obj_exn =
+ [ `WellTyped of NCic.obj
+ | `Exn of exn ]
+;;
+
+type db = {
+ cache : obj_exn NUri.UriHash.t;
+ history : item list ref;
+ frozen_list : (NUri.uri * NCic.obj) list ref;
+ lt_constraints : (NUri.uri * NUri.uri) list ref;
+ universes : NUri.uri list ref
+}
+
+class type g_status =
+ object
+ method env_db : db
+ end
+
+
+class virtual status uid =
+ object
+ inherit NCic.status uid
+
+ val db = {
+ cache = NUri.UriHash.create 313;
+ history = ref [];
+ frozen_list = ref [];
+ lt_constraints = ref []; (* a,b := a < b *)
+ universes = ref []
+ }
+
+ method env_db = db
+
+ method set_env_db v = {< db = v >}
+ method set_env_status : 's.#g_status as 's -> 'self
+ = fun o -> {< db = o#env_db >}
+ end
+;;
+
+let get_obj = ref (fun _ _ -> assert false);;