diff options
Diffstat (limited to 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 256abed6a1..ec59916e3c 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -16,10 +16,12 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool + : program_mode:bool -> ?hook:DeclareDef.Hook.t - -> Id.t - -> definition_kind + -> name:Id.t + -> scope:locality + -> poly:bool + -> kind:definition_object_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option |