Coq: fix non-mutually recursive functions with measures

rems-project · Nov 14, 2023 · 3f8a320 · 3f8a320
1 parent 435ffd3
commit 3f8a320
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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