summaryrefslogtreecommitdiff
path: root/src/Invariants.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index fec6b2ed..364c14d0 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -352,7 +352,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
- let def = T.TypeDefId.nth ctx.type_context def_id in
+ let def = C.ctx_lookup_type_def ctx def_id in
(* Check the number of parameters *)
assert (List.length regions = List.length def.region_params);
assert (List.length tys = List.length def.type_params);
@@ -435,7 +435,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
- let def = T.TypeDefId.nth ctx.type_context def_id in
+ let def = C.ctx_lookup_type_def ctx def_id in
(* Check the number of parameters *)
assert (List.length regions = List.length def.region_params);
assert (List.length tys = List.length def.type_params);