X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=5a708ceddb8deb46c9a91602c6652d95a814c8e3;hb=64d7a7dfa840d7279f9af64240ee1f8a69181801;hp=4272ccdc6002b4548be90ae81adbc0b67490d983;hpb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;p=helm.git diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 4272ccdc6..5a708cedd 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -285,7 +285,7 @@ let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () = in CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in - let obj_pp = CicNotationPp.pp_obj in + let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t in let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in