diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 5bf3350777..925a2d8389 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -283,9 +283,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in + let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in let _ : GlobRef.t list = - Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration + Declare.declare_mutually_recursive ~info ~uctx + ~possible_indexes:indexes ~ntns ~rec_declaration fixitems in () |