summaryrefslogtreecommitdiff
path: root/compiler/Contexts.ml
diff options
context:
space:
mode:
authorSon Ho2022-12-17 07:09:49 +0100
committerSon HO2023-02-03 11:21:46 +0100
commitd585060e227921e9f650f5dbcd308bf492d13583 (patch)
tree950081fabe9ea9e0078efcaa18bfa412f6fdb017 /compiler/Contexts.ml
parent9b37e05e4861375f40dfdd35472468354f21280c (diff)
Fix another bug
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 3d09b58a..f2fa36c5 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -491,6 +491,12 @@ let ctx_subst_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) (nabs : V.abs)
let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
({ ctx with env }, abs_opt)
+let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : V.AbstractionId.id)
+ (can_end : bool) : eval_ctx =
+ let abs = ctx_lookup_abs ctx abs_id in
+ let abs = { abs with can_end } in
+ fst (ctx_subst_abs ctx abs_id abs)
+
let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
match decl_group with Rec _ -> true | NonRec _ -> false