Merge PR #12178: Fix recursively vs corecursively defined message

Reviewed-by: ppedrot

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 601e7e060c..1809c2bc91 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -112,7 +112,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
          declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
       fixitems fixdecls
   in
-  let isfix = Option.is_empty possible_indexes in
+  let isfix = Option.has_some possible_indexes in
   let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
   Declare.recursive_message isfix indexes fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;