From 3f8a32030253291d391e915d6b0bedd628536398 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 14 Nov 2023 13:56:12 +0000 Subject: [PATCH] Coq: fix non-mutually recursive functions with measures --- src/sail_coq_backend/pretty_print_coq.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index d391a4f07..04268611e 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -2946,9 +2946,9 @@ let doc_funcl_init types_mod avoid_target_names effect_info mutrec rec_opt ?rec_ in let intropp = match mutrec with NotMutrec -> intropp | FirstFn -> string "Fixpoint" | LaterFn -> string "with" in let ctxt = - match mutrec with - | NotMutrec -> ctxt - | _ -> { ctxt with recursive_fns = Bindings.singleton id (List.length quantspp, 0, is_measured) } + match (rec_opt, mutrec) with + | Rec_aux (Rec_nonrec, _), NotMutrec -> ctxt + | _, _ -> { ctxt with recursive_fns = Bindings.singleton id (List.length quantspp, 0, is_measured) } in let _ = match guard with