Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
d461ec79
Commit
d461ec79
authored
Sep 21, 2011
by
Asma Tafat-Bouzid
Browse files
Latex statistics
parent
39342c3c
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/ide/replay.ml
View file @
d461ec79
...
...
@@ -330,14 +330,18 @@ let prover_name a =
|
M
.
Undetected_prover
s
->
s
let
rec
goal_latex_stat
n
fmt
prov
depth
depth_max
first
g
=
if
(
n
==
1
)
then
begin
if
(
n
==
1
)
then
begin
if
not
first
then
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
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
if
depth
>
0
then
fprintf
fmt
"&"
if
(
depth
<
depth_max
)
then
if
depth
>
0
then
fprintf
fmt
"&"
end
;
if
(
depth
<=
1
)
then
fprintf
fmt
"
\\
verb|%s| "
(
M
.
goal_expl
g
);
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment