diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 2 |
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; |