+(* *)
+(* Since the universes are not exported directly, but generated *)
+(* typecheking the library, we can't find them in the library as we *)
+(* do for the types. This means that when we commit uris during *)
+(* univ generation we can't associate the uri with the universe graph *)
+(* we find in the library, we have to calculate it and then inject it *)
+(* in the cacke. This is an orrible backdoor used by univ_maker. *)
+(* see the .ml file for some reassuring invariants *)
+val set_type_checking_info :
+ ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
+
+(* We need this in the Qed. *)
+val add_type_checked_term :
+ UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+
+ (** remove a type checked object
+ * @raise Object_not_found when given term is not in the environment
+ * @raise Failure when remove_term is invoked while type checking *)
+val remove_obj: UriManager.uri -> unit
+
+(* get_cooked_obj ~trust uri *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found *)
+val get_cooked_obj :
+ ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+ Cic.obj * CicUniv.universe_graph
+
+(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
+
+exception OnlyPutOfInductiveDefinitionsIsAllowed
+
+(* put_inductive_definition uri obj *)
+(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
+(* in the environment. *)
+(* WARNING: VERY UNSAFE. *)
+(* This function should be called only on a well-typed definition. *)
+val put_inductive_definition :
+ UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+
+(* (de)serialization *)
+val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
+val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
+val empty : unit -> unit
+
+(** Set trust function. Per default this function is set to (fun _ -> true) *)
+val set_trust: (UriManager.uri -> bool) -> unit
+
+ (** @return true for objects currently cooked/frozend/unchecked, false
+ * otherwise (i.e. objects already parsed from XML) *)
+val in_cache : UriManager.uri -> bool
+
+(* to debug the matitac batch compiler *)
+val list_obj: unit -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+val list_uri: unit -> UriManager.uri list
+
+ (** @return true for objects available in the library *)
+val in_library: UriManager.uri -> bool