diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-08 20:39:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-08 20:53:51 +0200 |
| commit | 0dfaecc2de2306ff9674a4aa3e546d3123015169 (patch) | |
| tree | d031ad991f690c7fa1f77213dcc8af0a9df27a0c /toplevel/command.mli | |
| parent | 2fceefe036f5f8289fd4667ade8b3240a11579d7 (diff) | |
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
the checker, and it was not used before that anyway.
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} *) |