added -noinnertypes

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index c71c24f11c109f46458ceb7c030a8e374b5f0bcf..c6682bd9100df786a88c71425230f8a219de07ed 100644 (file)
--- 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