X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=c6682bd9100df786a88c71425230f8a219de07ed;hb=84e4ed5e9a09589ac149c6d0d135c226d5b7a5f9;hp=c71c24f11c109f46458ceb7c030a8e374b5f0bcf;hpb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;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