else [])@
[GA.Executable(floc,GA.Tactic(floc, Some (
if ueq_case then
- GA.Auto (floc,["paramodulation","";
+ GA.AutoBatch (floc,["paramodulation","";
"timeout",string_of_int !paramod_timeout])
else
- GA.Auto (floc,["depth",string_of_int !depth])
+ GA.AutoBatch (floc,["depth",string_of_int !depth])
),
- GA.Dot(floc)));
+ GA.Semicolon(floc)));
GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
GA.Assumption floc)), GA.Dot(floc)))
]@
let pres_term = TermContentPres.pp_ast content_term in
let dummy_tbl = Hashtbl.create 1 in
let markup = CicNotationPres.render dummy_tbl pres_term in
- let s = BoxPp.render_to_string List.hd width markup in
+ let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
Pcre.substitute
~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
in
CicNotationPp.set_pp_term term_pp;
let lazy_term_pp = fun x -> assert false in
let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
- GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+ GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t
in
let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
let extra_statements_start = [