8 files changed, 23 insertions, 134 deletions

diff --git a/library/global.ml b/library/global.ml
index 28b691769..5425e5930 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -14,7 +14,17 @@ open Safe_typing
 (* We introduce here the global environment of the system, and we declare it
    as a synchronized table. *)
 
-let global_env = Summary.ref empty_environment ~name:"Global environment"
+let global_env = ref empty_environment
+
+let join_safe_environment () =
+  global_env := Safe_typing.join_safe_environment !global_env
+
+let () =
+  Summary.declare_summary "Global environment"
+    { Summary.freeze_function = (fun b ->
+        if b then join_safe_environment (); !global_env);
+      unfreeze_function = (fun fr -> global_env := fr);
+      init_function = (fun () -> global_env := empty_environment) }
 
 let safe_env () = !global_env
 
diff --git a/library/global.mli b/library/global.mli
index 3238294f2..a5ca92013 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -102,6 +102,8 @@ val import : compiled_library -> Digest.t ->
 val type_of_global : Globnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
+val join_safe_environment : unit -> unit
+
 (** spiwack: register/unregister function for retroknowledge *)
 val register : Retroknowledge.field -> constr -> constr -> unit
 
diff --git a/library/lib.ml b/library/lib.ml
index 47341e675..b4371812b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -523,85 +523,8 @@ let close_section () =
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
-(*****************)
-(* Backtracking. *)
-
-let (inLabel : int -> obj), (outLabel : obj -> int) =
-  declare_object_full {(default_object "DOT") with
-				classify_function = (fun _ -> Dispose)}
-
-let recache_decl = function
-  | (sp, Leaf o) -> cache_object (sp,o)
-  | (_,OpenedSection _) -> add_section ()
-  | _ -> ()
-
-let recache_context ctx =
-  List.iter recache_decl ctx
-
-let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
-
-let set_lib_stk new_lib_stk =
-  lib_stk := new_lib_stk;
-  recalc_path_prefix ();
-  (* Always at least one frozen state in the libstack *)
-  match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) ->
-      Summary.unfreeze_summaries f;
-      let (after,_,_) = split_lib sp in
-      recache_context after
-    | _ -> assert false
-
-let reset_to test =
-  let (_,_,before) = split_lib_gen test in
-  set_lib_stk before
-
-let first_command_label = 1
-
-let mark_end_of_command, current_command_label, reset_command_label =
-  let n = ref (first_command_label-1) in
-  (fun () ->
-    match !lib_stk with
-        (_,Leaf o)::_ when String.equal (object_tag o) "DOT" -> ()
-      | _ -> incr n;add_anonymous_leaf (inLabel !n)),
-  (fun () -> !n),
-  (fun x -> n:=x;add_anonymous_leaf (inLabel x))
-
-let is_label_n n x =
-  match x with
-    | (sp, Leaf o) when String.equal (object_tag o) "DOT" &&
-      Int.equal n (outLabel o) -> true
-    | _ -> false
-
-(** Reset the label registered by [mark_end_of_command()] with number n,
-    which should be strictly in the past. *)
-
-let reset_label n =
-  if n >= current_command_label () then
-    error "Cannot backtrack to the current label or a future one";
-  reset_to (is_label_n n);
-  (* forget state numbers after n only if reset succeeded *)
-  reset_command_label n
-
-let raw_reset_initial () = reset_label first_command_label
-
-(** Search the last label registered before defining [id] *)
-
-let label_before_name (loc,id) =
-  let found = ref false in
-  let search = function
-    | (_, Leaf o) when !found && String.equal (object_tag o) "DOT" -> true
-    | ((fp, _),_) ->
-      let (_, name) = repr_path fp in
-      let () = if Names.Id.equal id name then found := true in
-      false
-  in
-  match find_entry_p search with
-    | (_,Leaf o) -> outLabel o
-    | _ -> raise Not_found
-
 (* State and initialization. *)
 
 type frozen = Names.DirPath.t option * library_segment
@@ -616,8 +539,7 @@ let unfreeze (mn,stk) =
 let init () =
   unfreeze (None,[]);
   Summary.init_summaries ();
-  add_frozen_state (); (* Stores e.g. the keywords declared in g_*.ml4 *)
-  mark_end_of_command () (* For allowing Reset Initial in coqtop -l *)
+  add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
 
 (* Misc *)
 
diff --git a/library/lib.mli b/library/lib.mli
index a956ff5d0..04f8d0775 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,31 +147,6 @@ val remove_section_part : Globnames.global_reference -> Names.DirPath.t
 val open_section : Names.Id.t -> unit
 val close_section : unit -> unit
 
-(** {6 Backtracking } *)
-
-(** NB: The next commands are low-level ones, do not use them directly
-    otherwise the command history stack in [Backtrack] will be out-of-sync.
-    Also note that [reset_initial] is now [reset_label first_command_label] *)
-
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
-   [mark_end_of_command()]. It forgets anything registered after
-   this label. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
-(** [raw_reset_initial] is now [reset_label] to the first label.
-    This is meant to be used during initial Load's and compilations.
-    Otherwise, consider instead [Backtrack.reset_initial] *)
-val raw_reset_initial : unit -> unit
-
-(** search the label registered immediately before adding some definition *)
-val label_before_name : Names.Id.t Loc.located -> int
-
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
 type frozen
diff --git a/library/library.ml b/library/library.ml
index 472b1fb1d..0766a62d7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -44,17 +44,20 @@ module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
+let join x = Safe_typing.join_compiled_library x.library_compiled
 (* This is a map from names to loaded libraries *)
-let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
+let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l
+let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
 let libraries_filename_table = ref LibraryFilenameMap.empty
 
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
-let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
-let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
-let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
+let freeze b l = if b then (List.iter join l; l) else l
+let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze
+let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze
+let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze
 
 (* various requests to the tables *)
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 9f2bede75..fd27ef264 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -522,8 +522,8 @@ let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
   paresseusement : il faut forcer l'évaluation pour capturer
   l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
-  let s = string_of_qualid (shortest_qualid_of_global env ref) in
-  (str s)
+  try str (string_of_qualid (shortest_qualid_of_global env ref))
+  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
 
 let global_inductive r =
   match global r with
diff --git a/library/states.ml b/library/states.ml
index 1fd3fa2e5..93b2c120e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -32,17 +32,6 @@ let (extern_state,intern_state) =
 
 (* Rollback. *)
 
-let with_heavy_rollback f h x =
-  let st = freeze ~marshallable:false in
-  try
-    f x
-  with reraise ->
-    let e = h reraise in (unfreeze st; raise e)
-
-let without_rollback f h x =
-  try f x
-  with reraise -> raise (h reraise)
-
 let with_state_protection f x =
   let st = freeze ~marshallable:false in
   try
diff --git a/library/states.mli b/library/states.mli
index d186bf1c8..da6f33d65 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -22,18 +22,6 @@ val unfreeze : state -> unit
 
 (** {6 Rollback } *)
 
-(** [with_heavy_rollback f h x] applies [f] to [x]. If this application
-    ends on an exception, the wrapper [h] is applied to it, then
-    the state of the whole system is restored as it was before applying [f],
-    and finally the exception produced by [h] is raised. *)
-
-val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
-
-(** [without_rollback] is just like [with_heavy_rollback], except that
-    no state is restored in case of exception. *)
-
-val without_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
-
 (** [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before applying [f] *)