From 70b380dec94dd76f0df9e5f05c0d4d77992d3338 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 14 Jan 2025 14:03:51 +0000 Subject: [PATCH] fix in case of no register --- src/sail_lean_backend/pretty_print_lean.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index cc1c19557..7a391af61 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -553,7 +553,8 @@ let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o effect_inf let defs = remove_imports defs 0 in let global = { effect_info } in let ctxt = { empty_context with global } in - let register_refs = State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) (State.find_registers defs) in + let regs = State.find_registers defs in + let register_refs = match regs with [] -> empty | _ -> State.register_refs_lean (doc_id ctxt) (doc_typ ctxt) regs in let output : document = separate_map empty (doc_def ctxt) defs in print o (register_refs ^^ hardline ^^ output); ()