X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=8ae9b00a37fb0e325058428be5ade6bb957abc66;hb=488f49d2ac60fa63e65a19ad8684414266e05ac6;hp=c25113f26f1a32612ce41fc063a5cdb448c54125;hpb=92365dd290f8916cc2f6b09011134ffadf97f3ed;p=helm.git

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index c25113f26..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 *)
 ]
@@ -245,7 +246,7 @@ let parse_cmdline init_status =
       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
+      Helm_registry.set_bool "matita.noinnertypes" true in
     let arg_spec =
       let std_arg_spec = [
         "-I", Arg.String (add_l includes),