added support for dump/restore/clear proof checker cache

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index e93db958210ef5fa820d502f4317d2567f868a6c..99244f47f7c25e2bef0efe258507c9e5b49b81c0 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -77,3 +77,9 @@ exception OnlyPutOfInductiveDefinitionsIsAllowed
 (* 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
+