X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2FocamlExtraction.ml;h=6465aa86d26a57e9f68dcf30e640db202e792ed3;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=da7eee5acda96d889b57e25a8ff94dd3f7cb32f9;hpb=59dfa0b85ba8a74f4b5c175f72ac7ebeed6fca7f;p=helm.git diff --git a/matita/components/ng_extraction/ocamlExtraction.ml b/matita/components/ng_extraction/ocamlExtraction.ml index da7eee5ac..6465aa86d 100644 --- a/matita/components/ng_extraction/ocamlExtraction.ml +++ b/matita/components/ng_extraction/ocamlExtraction.ml @@ -18,8 +18,9 @@ let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) = status,()) res in status with - HExtlib.Localized (_,exn) -> - prerr_endline (Printexc.to_string exn); assert false + HExtlib.Localized (_,exn) + | exn -> + prerr_endline (Printexc.to_string exn); assert false let do_if_ocaml_set f status = if try ignore (Helm_registry.get "extract_ocaml"); true @@ -40,6 +41,7 @@ let print_open status uris = List.map (fun uri -> Filename.basename (NUri.string_of_uri uri)) uris in let status,cmds = map_status status Ocaml.pp_open fnames in List.iter (print_ppcmds status ~in_ml:true) cmds; + let status,cmds = map_status status Ocaml.pp_open fnames in List.iter (print_ppcmds status ~in_ml:false) cmds; status ) status