diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index edf7ed9dc3..9708f43e53 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,12 +69,15 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref -let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = - CList.map4 - (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque ~types ~univs body in - declare_definition ~name ~scope ~kind ~ubind ~impargs ce) - fixnames fixdecls fixtypes fiximps +let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = + let csts = CList.map4 + (fun name body types impargs -> + let ce = Declare.definition_entry ~opaque ~types ~univs body in + declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + fixnames fixdecls fixtypes fiximps + in + Declare.recursive_message (not cofix) indexes fixnames; + csts let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" |