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
2ab8c14e
Commit
2ab8c14e
authored
Jul 01, 2016
by
Martin Clochard
Browse files
compute: fix correction bug related to typing corner cases
parent
c0e2fdb3
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/transform/reduction_engine.ml
View file @
2ab8c14e
...
...
@@ -330,8 +330,12 @@ let first_order_matching (vars : Svs.t) (largs : term list)
begin
match
t2
.
t_node
with
|
Tapp
(
ls2
,
args2
)
when
ls_equal
ls1
ls2
->
loop
sigma
(
List
.
rev_append
args1
r1
)
(
List
.
rev_append
args2
r2
)
let
mt
,
mv
=
loop
sigma
(
List
.
rev_append
args1
r1
)
(
List
.
rev_append
args2
r2
)
in
begin
try
Ty
.
oty_match
mt
t1
.
t_ty
t2
.
t_ty
,
mv
with
Ty
.
TypeMismatch
_
->
raise
NoMatch
end
|
_
->
raise
NoMatch
end
|
_
->
...
...
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