diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 8406edcb6..bfa9e3978 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -533,8 +533,9 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat => /* Determines whether any term is in an error hole. */ let is_error = (ci: t): bool => { switch (ci) { - | InfoExp({mode, self, ctx, _}) => - switch (status_exp(ctx, mode, self)) { + | InfoExp({status, _}) => + // TODO Confirm with disconcision that we can use the derived status + switch (status) { | InHole(_) => true | NotInHole(_) => false } diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index d9c5e6c10..71e081038 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -828,7 +828,7 @@ and uexp_to_info_map = let (term, rewrap) = UExp.unwrap(uexp); let og_exp = Exp.fresh(term); - let (_, m) = + let (og_info, m) = uexp_to_info_map( ~ctx, ~mode=Mode.Ana(ana_ty), @@ -841,8 +841,12 @@ and uexp_to_info_map = rewrap( Tuple([TupLabel(Label(l1) |> Exp.fresh, og_exp) |> Exp.fresh]), ); + let (info, m) = + uexp_to_info_map(~ctx, ~mode, ~ancestors, fake_uexp, m); - uexp_to_info_map(~ctx, ~mode, ~ancestors, fake_uexp, m); + let info = {...info, status: og_info.status}; + + (info, add_info(fake_uexp.ids, InfoExp(info), m)); }; | _ => default_case() }