Skip to content

Commit

Permalink
Coq: add full type information to environment during E_app processing
Browse files Browse the repository at this point in the history
Fixes phantom_bitlist_union test.
  • Loading branch information
bacam committed Jan 16, 2025
1 parent 41348ac commit 07dc311
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/sail_coq_backend/pretty_print_coq.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1715,7 +1715,7 @@ let doc_exp, doc_let =
| Typ_aux (Typ_fn (arg_typs, ret_typ), _) -> (arg_typs, ret_typ)
| _ -> raise (Reporting.err_unreachable l __POS__ "Function not a function type")
in
let fn_typ_env = List.fold_left (fun env kopt -> Env.add_typ_var l kopt env) env (quant_kopts tqs) in
let fn_typ_env = Env.add_typquant l tqs env in
let is_monadic = not (Effects.function_is_pure f ctxt.global.effect_info) in
let inst, inst_env =
(* We attempt to get an instantiation of the function signature's
Expand Down

0 comments on commit 07dc311

Please sign in to comment.