X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;fp=components%2Flibrary%2FlibrarySync.ml;h=630b51be8a59c4352cf4fe92bbf5d716f6891d1f;hb=f06968e452cca8782e822d98bec9007404abcbbe;hp=c36d84c90dd88de02938fdef9507906a55659edb;hpb=94267002fc18aa42a8c09779ad6485f93c3e90fa;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index c36d84c90..630b51be8 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -243,6 +243,29 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
+let stack = ref [];;
+
+let h2l h =
+  UriManager.UriHashtbl.fold 
+  (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+  remove_all_coercions ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP from librarySync.ml")
+  | (db,h) :: tl -> 
+      stack := tl;
+      remove_all_coercions ();
+      CoercDb.restore db;
+      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+      h
+;;
+
 let add_coercion ~add_composites refinement_toolkit uri arity saturations
  baseuri
 =