Commit 1a364000 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Pdecl: relax type constraints on invariant witnesses

parent 3a8adda5
......@@ -92,7 +92,8 @@ let create_plain_record_decl ~priv ~mut id args fdl invl witn =
"This expression may not terminate, it cannot be a witness";
if not (eff_pure e.e_effect) then Loc.errorm ?loc
"This expression has side effects, it cannot be a witness";
Loc.try2 ?loc ity_equal_check e.e_ity fd.pv_ity) fdl witn
let ety = ty_of_ity e.e_ity and fty = fd.pv_vs.vs_ty in
Loc.try2 ?loc ty_equal_check ety fty) fdl witn
mk_itd s pjl csl invl witn
......@@ -963,8 +963,8 @@ let add_types muc tdl =
| Qdot _ -> raise Not_found
with Not_found -> Loc.errorm ~loc:(qloc q)
"Unknown field %a" print_qualid q in
let dity = dity_of_ity v.pv_ity in
let de = dexpr muc denv_empty e in
let dity = snd (Dexpr.dexpr (DEsym (PV v))).de_dvty in
let de = Dexpr.dexpr ?loc:de.de_loc (DEcast (de, dity)) in
Mpv.add v (expr ~keep_loc:true de) m in
let wit = List.fold_left add_w Mpv.empty d.td_wit 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