From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Nov 2007 08:49:23 +0000 (+0000)
Subject: added -noinnertypes
X-Git-Tag: make_still_working~5828
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92365dd290f8916cc2f6b09011134ffadf97f3ed;p=helm.git

added -noinnertypes
---

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index c71c24f11..c6682bd91 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/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/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 6ef5a3bc4..c25113f26 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/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";