Commit 55e8f989 authored by Andrei Paskevich's avatar Andrei Paskevich

Vc: minor

parent ce0b3584
......@@ -266,14 +266,14 @@ let decrease_def env loc old_t t =
if ty_equal (t_type old_t) ty then
match ty.ty_node with
| Tyapp (ts,_) when ts_equal ts ts_int ->
t_and (ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
t_and (ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
| Tyapp (ts, _) when is_range_type_def ts.ts_def ->
let ls = int_of_range env ts in
let proj t = fs_app ls [t] ty_int in
ps_app env.ps_int_lt [proj t; proj old_t]
let ls = int_of_range env ts in
let proj t = fs_app ls [t] ty_int in
ps_app env.ps_int_lt [proj t; proj old_t]
| _ ->
decrease_alg env loc old_t t
decrease_alg env loc old_t t
else decrease_alg env loc old_t t
let decrease env loc attrs expl olds news =
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment