aboutsummaryrefslogtreecommitdiff
path: root/library/lib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.mli')
-rw-r--r--library/lib.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli
index d1b4977dd5..30569197bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -148,9 +148,12 @@ val close_section : unit -> unit
type frozen
-val freeze : marshallable:Summary.marshallable -> frozen
+val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
+(** Keep only the libobject structure, not the objects themselves *)
+val drop_objects : frozen -> frozen
+
val init : unit -> unit
(** {6 Section management for discharge } *)