diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 41cb5baa3..e48a77000 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -34,11 +34,11 @@ val interp_definition : val declare_definition : Id.t -> definition_kind -> definition_entry -> Impargs.manual_implicits -> - Globnames.global_reference declaration_hook -> Globnames.global_reference + Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> unit declaration_hook -> unit + constr_expr option -> unit Lemmas.declaration_hook -> unit (** {6 Parameters/Assumptions} *) |