we parametrized CicNotationPt.obj on 'term

[helm.git] / components / tptp_grafite / tptp2grafite.ml

diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml
index 4272ccdc6002b4548be90ae81adbc0b67490d983..5a708ceddb8deb46c9a91602c6652d95a814c8e3 100644 (file)
--- a/components/tptp_grafite/tptp2grafite.ml
+++ b/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