Helm_registry.set_bool "matita.system" true),
("Act on the system library instead of the user one"
^ "\n WARNING: not for the casual user");
Helm_registry.set_bool "matita.system" true),
("Act on the system library instead of the user one"
^ "\n WARNING: not for the casual user");