Commit e97f94ab authored by MARCHE Claude's avatar MARCHE Claude

ITP: print explanation between square brackets

parent 1fddf96b
...@@ -682,9 +682,9 @@ end ...@@ -682,9 +682,9 @@ end
String.sub full 0 40 ^ " ..." String.sub full 0 40 ^ " ..."
else full else full
| APn pn -> | APn pn ->
let name = (get_proof_name d.cont.controller_session pn).Ident.id_string in
let expl = get_proof_expl d.cont.controller_session pn in let expl = get_proof_expl d.cont.controller_session pn in
if expl <> "" then expl else if expl = "" then name else name ^ " [" ^ expl ^ "]"
(get_proof_name d.cont.controller_session pn).Ident.id_string
| APa pa -> | APa pa ->
let pa = get_proof_attempt_node d.cont.controller_session pa in let pa = get_proof_attempt_node d.cont.controller_session pa in
Pp.string_of Whyconf.print_prover pa.prover Pp.string_of Whyconf.print_prover pa.prover
......
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