This commit is contained in:
adelaett 2023-02-13 14:54:47 +01:00
parent 363ef39704
commit 0262019d45
2 changed files with 4 additions and 10 deletions

View File

@ -384,10 +384,10 @@ and translate_hoists ~append_esome ctx hoists kont =
let new_mark : typed mark =
match mark_hoist with Typed m -> Typed { m with ty = TAny, pos }
in
Expr.make_app'
Expr.make_app ~decl_ctx:(Some ctx.decl_ctx)
(Expr.make_var (Var.translate A.handle_default_opt) new_mark)
[Expr.earray excepts' new_mark; just'; cons']
pos ctx.decl_ctx
pos
| ELit LEmptyError -> A.make_none mark_hoist
| EApp { f; args } ->
let f = translate_expr ctx f in
@ -400,7 +400,7 @@ and translate_hoists ~append_esome ctx hoists kont =
A.make_bind_cont mark_hoist f (fun f ->
A.make_bindm_cont mark_hoist args (fun args ->
Expr.make_app' f args pos ctx.decl_ctx
Expr.make_app ~decl_ctx:(Some ctx.decl_ctx) f args pos
(* A.make_bind_cont mark_hosit (Expr.make_app f args pos) *)))
(* assert false *)
| EAssert arg ->

View File

@ -260,18 +260,12 @@ val make_abs :
('a, 'm mark) boxed_gexpr
val make_app :
?decl_ctx:decl_ctx option ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
Pos.t ->
('a, 'm mark) boxed_gexpr
val make_app' :
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
Pos.t ->
decl_ctx ->
('a, 'm mark) boxed_gexpr
val empty_thunked_term :
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) boxed_gexpr