Commit f5f8599c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed typing of for loop index

parent 2f7b69b5
......@@ -1317,7 +1317,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEfor (id,de_from,dir,de_to,dinv,de) ->
let e_from = expr uloc env de_from in
let e_to = expr uloc env de_to in
let v = create_pvsymbol id ity_int in
let v = create_pvsymbol id e_from.e_ity in
let env = add_pvsymbol env v in
let i = if ity_equal v.pv_ity ity_int then v else
create_pvsymbol id ~ghost:true ity_int in
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