added -noinnertypes

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

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index 6ef5a3bc4a0874e722ec638abe6e37dcbac96bc2..c25113f26f1a32612ce41fc063a5cdb448c54125 100644 (file)
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -244,6 +244,8 @@ let parse_cmdline init_status =
     let increase_verbosity () =
       Helm_registry.set_int "matita.verbosity"
         (Helm_registry.get_int "matita.verbosity" + 1) in
+    let no_innertypes () =
+      Helm_registry.set_bool "matita.noinnertypes" false in
     let arg_spec =
       let std_arg_spec = [
         "-I", Arg.String (add_l includes),
@@ -259,6 +261,8 @@ let parse_cmdline init_status =
         "-noprofile", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
           "Turns off profiling printings";
+        "-noinnertypes", Arg.Unit no_innertypes, 
+          "Turns off inner types generation while publishing";
         "-profile-only",
           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
           "Activates only profiler with label matching the provided regex";