X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=8ae9b00a37fb0e325058428be5ade6bb957abc66;hb=66faca1dc849662e27d760b950294ef66a5741b3;hp=6ef5a3bc4a0874e722ec638abe6e37dcbac96bc2;hpb=47ac62b2a4852b82598acd6ac2a9cd0654aa2748;p=helm.git

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 6ef5a3bc4..8ae9b00a3 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -50,7 +50,8 @@ let registry_defaults = [
   "matita.system",               "false";
   "matita.verbosity",            "1";
   "matita.bench",                "false";
-  "matita.paste_unicode_as_tex", "false"
+  "matita.paste_unicode_as_tex", "false";
+  "matita.noinnertypes",         "false";
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]
@@ -244,6 +245,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" true in
     let arg_spec =
       let std_arg_spec = [
         "-I", Arg.String (add_l includes),
@@ -259,6 +262,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";