modifications to make matita behave reasonably, removed some useless windows

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

diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml
index ca3d873c5f563dd4917736b49a98a7d17ba058f1..b024811116ba011ee1ffd618515e214c27d0fa61 100644 (file)
--- a/components/grafite_engine/grafiteSync.ml
+++ b/components/grafite_engine/grafiteSync.ml
@@ -139,7 +139,7 @@ let init baseuri =
   {
     GrafiteTypes.moo_content_rev = [];
     proof_status = GrafiteTypes.No_proof;
-    options = GrafiteTypes.no_options;
+(*     options = GrafiteTypes.no_options; *)
     objects = [];
     coercions = [];
     universe = Universe.empty;