From 1172b52735a299dfc91aee36b30b576dfeff581c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 21:26:48 +0100 Subject: [flags] Make program_mode a parameter for commands in vernac. This is useful as it allows to reflect program_mode behavior as an attribute. --- vernac/comDefinition.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/comDefinition.mli') 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 -- cgit v1.2.3