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
5104cd07
Commit
5104cd07
authored
May 10, 2010
by
Simon Cruanes
Browse files
bugfix for f_neq special case
parent
ba8f3677
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/core/term.ml
View file @
5104cd07
...
...
@@ -505,12 +505,12 @@ let ps_neq =
let
v
=
ty_var
(
create_tvsymbol
(
id_fresh
"a"
))
in
create_psymbol
(
id_fresh
"infix <>"
)
[
v
;
v
]
let
f_equ
t1
t2
=
f_app
ps_equ
[
t1
;
t2
]
let
f_neq
t1
t2
=
f_app
ps_neq
[
t1
;
t2
]
let
f_app
p
tl
=
if
ls_equal
p
ps_neq
then
f_not
(
f_app
ps_equ
tl
)
else
f_app
p
tl
let
f_equ
t1
t2
=
f_app
ps_equ
[
t1
;
t2
]
let
f_neq
t1
t2
=
f_app
ps_neq
[
t1
;
t2
]
let
f_app_unsafe
=
f_app
let
fs_tuple
n
=
...
...
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