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
e8374d94
Commit
e8374d94
authored
Aug 03, 2012
by
Jean-Christophe Filliâtre
Browse files
fixed WP of lambda expressions
parent
e3de235a
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/whyml/mlw_wp.ml
View file @
e8374d94
...
...
@@ -837,8 +837,9 @@ and wp_abstract env c_eff c_q c_xq q xq =
and
wp_fun_defn
env
lr
{
fun_ps
=
ps
;
fun_lambda
=
l
}
=
let
lab
=
fresh_mark
()
in
let
regs
=
ps
.
ps_subst
.
ity_subst_reg
in
let
regs
=
Mreg
.
map
(
fun
_
->
()
)
regs
in
let
add_arg
sbs
pv
=
ity_match
sbs
pv
.
pv_vtv
.
vtv_ity
pv
.
pv_vtv
.
vtv_ity
in
let
subst
=
List
.
fold_left
add_arg
ps
.
ps_subst
l
.
l_args
in
let
regs
=
Mreg
.
map
(
fun
_
->
()
)
subst
.
ity_subst_reg
in
let
args
=
List
.
map
(
fun
pv
->
pv
.
pv_vs
)
l
.
l_args
in
let
env
=
if
lr
=
0
||
l
.
l_variant
=
[]
then
env
else
let
lab
=
t_var
lab
in
...
...
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