- most of cic/ removed

[helm.git] / matita / components / grafite_engine / grafiteSync.ml

diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml
index 60c366a0ef2dec921adf0acbc6accbe998b0e011..9302cbf897c74a5a292b63fb6b5261cd1c5d36b4 100644 (file)
--- a/matita/components/grafite_engine/grafiteSync.ml
+++ b/matita/components/grafite_engine/grafiteSync.ml
@@ -74,11 +74,9 @@ let time_travel  ~present ?(past=initial_status present present#baseuri) () =
 let init lexicon_status =
   initial_status lexicon_status
   ;;
-let pop () =
-  LibraryObjects.pop ()
+let pop () = ()
 ;;
 
-let push () =
-  LibraryObjects.push ()
+let push () = ()
 ;;