diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:36:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:36:24 +0100 |
| commit | d73fee2674999225ce59cc0a9f61dfafe99d7689 (patch) | |
| tree | 2501d86e9ff5166d31662de6b4fd1b0bc1679033 /plugins/funind/indfun_common.mli | |
| parent | df2757b19b2be69aa2e026343221dbe185e3a0df (diff) | |
| parent | e3e4687715ee2839f4d326cb225ba4a586b8a48a (diff) | |
Merge PR #8999: [pfedit] Remove cook_proof stub.
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 0c8f40c5cf..c9d153d89f 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> Lemmas.declaration_hook CEphemeron.key -> unit -(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and - abort the proof -*) -val get_proof_clean : bool -> - Names.Id.t * - (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) - - - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings |