X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaInit.ml;h=c25113f26f1a32612ce41fc063a5cdb448c54125;hb=84e4ed5e9a09589ac149c6d0d135c226d5b7a5f9;hp=6ef5a3bc4a0874e722ec638abe6e37dcbac96bc2;hpb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;p=helm.git

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index 6ef5a3bc4..c25113f26 100644
--- 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";