fix in case of no register

lfrenot · Jan 14, 2025 · 70b380d · 70b380d
1 parent 5027c67
commit 70b380d
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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);
   ()