Commit cc55577d authored by David Hauzar's avatar David Hauzar

The parameter cntexample in Driver.print_task made optional.

parent 7bef376b
......@@ -1279,7 +1279,7 @@ let why3tac ?(timelimit=timelimit) s gl =
let cp, drv = get_prover s in
let command = String.concat " " (cp.command :: cp.extra_options) in
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task ~cntexample:false drv) !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let call = Driver.prove_task ~command ~timelimit drv !task () in
let res = wait_on_call call () in
match res.pr_answer with
......
......@@ -308,14 +308,14 @@ let print_task_prepared ?old drv fmt task =
fprintf fmt "@[%a@]@?" (printer ?old) task;
printer_args.printer_mapping
let print_task ?old ~cntexample drv fmt task =
let print_task ?old ?(cntexample=false) drv fmt task =
let task = prepare_task ~cntexample drv task in
let _ = print_task_prepared ?old drv fmt task in
()
let print_theory ?old drv fmt th =
let task = Task.use_export None th in
print_task ?old ~cntexample:false drv fmt task
print_task ?old drv fmt task
let prove_task_prepared
~command ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
......
......@@ -47,7 +47,7 @@ val call_on_buffer :
val print_task :
?old : in_channel ->
cntexample : bool ->
?cntexample : bool ->
driver -> Format.formatter -> Task.task -> unit
val print_theory :
......
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