Synchronizing loadpath with the backtrack mechanism.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 2 deletions

diff --git a/library/loadpath.ml b/library/loadpath.ml
index 44b53c09a..315cbf96e 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -20,12 +20,18 @@ type t = {
   path_is_root : bool;
 }
 
+let load_paths = ref ([] : t list)
+
+let () = Summary.declare_summary "LOADPATHS" {
+  Summary.freeze_function = (fun () -> !load_paths);
+  Summary.unfreeze_function = (fun l -> load_paths := l);
+  Summary.init_function = (fun () -> load_paths := []);
+}
+
 let logical p = p.path_logical
 
 let physical p = p.path_physical
 
-let load_paths = ref ([] : t list)
-
 let get_load_paths () = !load_paths
 
 let get_paths () = List.map physical !load_paths