1 files changed, 57 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli
new file mode 100644
index 000000000..80f61ef40
--- /dev/null
+++ b/library/lib.mli
@@ -0,0 +1,57 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Libobject
+open Summary
+(*i*)
+
+(* This module provides a general mechanism to keep a trace of all operations
+   and to backtrack (undo) those operations. It provides also the section
+   mechanism (at a low level; discharge is not known at this step). *)
+
+type node = 
+  | Leaf of obj
+  | OpenedSection of string * module_p
+  | ClosedSection of string * module_p * library_segment
+  | FrozenState of Summary.frozen
+
+and library_segment = (section_path * node) list
+
+and module_p = bool
+
+type library_entry = section_path * node
+
+
+(*s Adding operations, and getting the current list of operations (most 
+  recent ones come first). *)
+
+val add_leaf : identifier -> obj -> section_path
+val add_anonymous_leaf : obj -> unit
+
+val contents_after : section_path option -> library_segment
+
+
+(*s Opening and closing a section. *)
+
+val open_section : string -> bool -> section_path
+val close_section : string -> unit
+
+val make_path : identifier -> path_kind -> section_path
+val cwd : unit -> string list
+
+
+(*s Backtracking (undo). *)
+
+val reset_to : section_path -> unit
+
+
+(*s We can get and set the state of the operations (used in [States]). *)
+
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+
+val init : unit -> unit