Commit 46ba2d40 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

Latex statistics

parent d461ec79
......@@ -332,17 +332,29 @@ let prover_name a =
let rec goal_latex_stat n fmt prov depth depth_max first g =
if(n ==1) then
begin
if not first then
begin
if(depth < depth_max) then
for i = 1 to depth do fprintf fmt "&" done
if depth_max > 1 then
begin
if not first then
begin
if(depth < depth_max) then
for i = 1 to depth do fprintf fmt "&" done
else
for i = 1 to depth - 1 do fprintf fmt "&" done
end
else
for i = 1 to depth - 1 do fprintf fmt "&" done
end
else
if(depth < depth_max) then
if depth > 0 then fprintf fmt "&"
end;
if(depth < depth_max) then
if depth > 0 then fprintf fmt "&"
end
else
begin
if not first then
for i = 1 to depth do fprintf fmt "&" done
else
if depth > 0 then fprintf fmt "&"
end
end
else
for i = 1 to depth do fprintf fmt "\\quad" done;
if (depth <= 1) then
fprintf fmt "\\verb|%s| " (M.goal_expl g);
let proofs = M.external_proofs g 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