Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
433aaefd
Commit
433aaefd
authored
May 06, 2010
by
Francois Bobot
Browse files
main.ml : Ajout de ~debug pour print_task
parent
95c2ea8f
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/main.ml
View file @
433aaefd
...
...
@@ -277,7 +277,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
(
task_goal
task
)
.
Decl
.
pr_name
.
Ident
.
id_long
Call_provers
.
print_prover_result
res
|
None
,
None
->
Prover
.
print_task
drv
std_formatter
task
Prover
.
print_task
~
debug
drv
std_formatter
task
|
Some
dir
,
_
->
let
fname
=
Filename
.
basename
fname
in
let
fname
=
...
...
@@ -290,7 +290,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let
name
=
Ident
.
string_unique
!
fname_printer
(
String
.
sub
dest
0
i
)
in
let
ext
=
String
.
sub
dest
i
(
String
.
length
dest
-
i
)
in
let
cout
=
open_out
(
Filename
.
concat
dir
(
name
^
ext
))
in
Prover
.
print_task
drv
(
formatter_of_out_channel
cout
)
task
;
Prover
.
print_task
~
debug
drv
(
formatter_of_out_channel
cout
)
task
;
close_out
cout
let
do_theory
env
drv
fname
tname
th
glist
=
...
...
Write
Preview
Markdown
is supported
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