diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 23:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 22:52:32 +0200 |
| commit | c8883873426c92778a1cac02da17e3d123beb394 (patch) | |
| tree | 9ffcf82e3787d11c447851dd850ec1cdd4d3611d /plugins | |
| parent | 27fd525445e8ab37e67eebfb2bca1963e33c7f64 (diff) | |
[vernac] Remove unused abstraction from declaration_hook type.
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7e52ee224f..1b4c1248a5 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook CEphemeron.key -> unit + Lemmas.declaration_hook CEphemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof |