Commit d2d1fc90 authored by Andrei Paskevich's avatar Andrei Paskevich

rename printer "tptp" to "tptp-fof"

parent 8c03571f
...@@ -248,10 +248,10 @@ install-all: install install-lib ...@@ -248,10 +248,10 @@ install-all: install install-lib
PLUGGENERATED = PLUGGENERATED =
PLUG_PARSER = genequlin PLUG_PARSER = genequlin
PLUG_PRINTER = tptp PLUG_PRINTER = tptpfof
PLUG_TRANSFORM = PLUG_TRANSFORM =
PLUGINS = genequlin tptp PLUGINS = genequlin tptpfof
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \ PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \ $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
......
(* Why driver for first-order tptp provers *) (* Why driver for first-order tptp provers *)
printer "tptp" printer "tptp-fof"
filename "%f-%t-%g.p" filename "%f-%t-%g.p"
valid "Proof found" valid "Proof found"
......
(* Why driver for first-order tptp provers *) (* Why driver for first-order tptp provers *)
printer "tptp" printer "tptp-fof"
filename "%f-%t-%g.p" filename "%f-%t-%g.p"
valid "Refutation found" valid "Refutation found"
......
...@@ -148,7 +148,7 @@ let print_task pr thpr fmt task = ...@@ -148,7 +148,7 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) ignore (print_list_opt (add_flush newline2)
(print_decl info) fmt (Task.task_decls task)) (print_decl info) fmt (Task.task_decls task))
let () = register_printer "tptp" let () = register_printer "tptp-fof"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment