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
bfe30ee3
Commit
bfe30ee3
authored
Jun 15, 2010
by
Francois Bobot
Browse files
inline : Fix : the return value can also contain type variable
alt-ergo : trigger pas sur l'égalité
parent
5d47822f
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/printer/alt_ergo.ml
View file @
bfe30ee3
...
...
@@ -129,7 +129,8 @@ and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
and
print_triggers
drv
fmt
tl
=
let
filter
=
function
|
Term
_
|
Fmla
{
f_node
=
Fapp
_
}
->
true
|
Term
_
->
true
|
Fmla
{
f_node
=
Fapp
(
ps
,_
)}
->
not
(
ls_equal
ps
ps_equ
)
|
_
->
false
in
let
tl
=
List
.
map
(
List
.
filter
filter
)
tl
in
...
...
src/transform/inlining.ml
View file @
bfe30ee3
...
...
@@ -47,6 +47,7 @@ let rec replacet env t =
(
Ty
.
ty_match
mt
x
.
vs_ty
y
.
t_ty
,
Mvs
.
add
x
y
mv
)
in
let
(
mt
,
mv
)
=
List
.
fold_left2
add
(
Ty
.
Mtv
.
empty
,
Mvs
.
empty
)
vs
tl
in
let
mt
=
Ty
.
ty_match
mt
(
of_option
fs
.
ls_value
)
t
.
t_ty
in
t_ty_subst
mt
mv
t
with
Not_found
->
t
end
|
_
->
t
...
...
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