(* again in the future (is_type_checked will return true) *)
val set_type_checking_info : UriManager.uri -> unit
+(* We need this in the Qed. *)
+val add_type_checked_term : UriManager.uri -> Cic.obj -> 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) *)
(* WARNING: VERY UNSAFE. *)
(* This function should be called only on a well-typed definition. *)
val put_inductive_definition : UriManager.uri -> Cic.obj -> 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
+
+(* for filtering in tacticChaser *)
+(* NEW *)
+val in_cache : UriManager.uri -> bool