+let activate_extraction baseuri fname =
+ if Helm_registry.get_bool "matita.extract" then
+ let mangled_baseuri =
+ let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+ let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+ String.uncapitalize baseuri in
+ let f =
+ open_out
+ (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
+ LibrarySync.set_object_declaration_hook
+ (fun _ obj ->
+ output_string f (CicExportation.ppobj baseuri obj);
+ flush f);
+;;
+