Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
e8a48006
Commit
e8a48006
authored
Jan 23, 2016
by
Martin Clochard
Browse files
split: remove careless simplifications on patternmatchings (caused failure)
parent
15e18f71
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
5 additions
and
5 deletions
+5
5
src/transform/split_goal.ml
src/transform/split_goal.ml
+5
5
No files found.
src/transform/split_goal.ml
View file @
e8a48006
...
...
@@ 336,11 +336,11 @@ let rec split_core sp f =
List
.
fold_left
(
fun
(
cseen
,
pos
,
neg
,
side
)
(
p
,
_
,
sf
)
>
let
cseen
,
vl
,
cond
=
pat_condition
kn
tv
cseen
p
in
let
cond
=
if
ro
then
fold_cond
cond
else
cond
in
let
ps
cond
f
=

t_forall_close_simp
vl
[]
(
t_implies_simp
cond
f
)
in
let
ng
cond
f
=

t_exists_close_simp
vl
[]
(
t_and_simp
cond
f
)
in
let
ngt
_
a
=

t_not
a
and
tag
_
a
=

a
in
let
fcl
t
=

t_forall_close_simp
vl
[]
t
in
let
ecl
t
=

t_exists_close_simp
vl
[]
t
in
let
ps
cond
f
=
fcl
(
t_implies_simp
cond
f
)
in
let
ng
cond
f
=
ecl
(
t_and_simp
cond
f
)
in
let
ngt
_
a
=
fcl
(
t_not
a
)
and
tag
_
a
=
ecl
a
in
let
pos
=
pos
++
bimap
ngt
ps
cond
sf
.
pos
in
let
neg
=
neg
++
bimap
tag
ng
cond
sf
.
neg
in
let
side
=
side
++
bimap
ngt
ps
cond
sf
.
side
in
...
...
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