X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=c6682bd9100df786a88c71425230f8a219de07ed;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=c71c24f11c109f46458ceb7c030a8e374b5f0bcf;hpb=f38af523cd051d4c1d0dceeb59ce2fbbfc87367d;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index c71c24f11..c6682bd91 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -75,7 +75,9 @@ let save_object_to_disk uri obj ugraph univlist =
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
-   if Helm_registry.get_bool "matita.system" then
+   if Helm_registry.get_bool "matita.system" &&
+      not (Helm_registry.get_bool "matita.noinnertypes")
+   then
     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
      Cic2acic.acic_object_of_cic_object obj 
     in