diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 09582f4ef2..edf7ed9dc3 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,6 +69,13 @@ 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 warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ |