- let annobj, innertypes =
- if Helm_registry.get_bool "matita.system" then
- let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+ let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
+ 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, _, _ =