From 0c168436d42ebfb52bd0c3286d2634fe46671046 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Sat, 25 Apr 2020 16:14:18 -0500
Subject: Fix recursively vs corecursively defined message

Closes #12177.
---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;
-- 
cgit v1.2.3