diff options
Diffstat (limited to 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 8dcd31f25..4a65c1e91 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -14,7 +14,8 @@ open Constrexpr (** {6 Definitions/Let} *) -val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> +val do_definition : program_mode:bool -> + Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit |