Commit 898e8cfa authored by MARCHE Claude's avatar MARCHE Claude

itp

parent c47db2e2
......@@ -85,7 +85,7 @@ let build_prover_call c id pr limit callback =
~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let task = Session_itp.get_task c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:false ~inplace:false ~command
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
~limit driver task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
......
......@@ -401,13 +401,7 @@ let parse_transformation_arg args : Term.term option =
(* temporary : parses the term *)
match args with
| [s] ->
let s =
let l = String.length s in
if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
String.sub s 1 (l - 2)
else s
in
printf "parsing string \"%s\"@." s;
printf "parsing string '%s'@." s;
begin try
let lb = Lexing.from_string s in
let t = Lexer.parse_term lb in
......
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