From 92365dd290f8916cc2f6b09011134ffadf97f3ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Nov 2007 08:49:23 +0000 Subject: [PATCH] added -noinnertypes --- helm/software/components/library/librarySync.ml | 4 +++- helm/software/matita/matitaInit.ml | 4 ++++ 2 files changed, 7 insertions(+), 1 deletion(-) 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"; -- 2.39.2