]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tptp_grafite/tptp2grafite.ml
- Procedural convertible rewrites in the conclusion are now detected and replaced...
[helm.git] / helm / software / components / tptp_grafite / tptp2grafite.ml
index e2a05e1c79814016d6efa1f4eef9a1412ce0ca39..10ed2bc720fa8420eee1f09b7cd69763bd59363f 100644 (file)
@@ -370,7 +370,7 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
     match raw_preamble with
     | None -> 
        pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,false,"logic/equality.ma"))))
+           GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
     | Some s -> s buri
   in
   let extra_statements_end = [] in