diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 14:40:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 14:42:42 +0200 |
| commit | 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 (patch) | |
| tree | b75dbe069252890885fe7929aa8614e40b631359 /stm/lemmas.mli | |
| parent | 875f235dd0413faa34f7d46afc25d2eb90e386e5 (diff) | |
Cleanup API, making inference_hook optional
Diffstat (limited to 'stm/lemmas.mli')
| -rw-r--r-- | stm/lemmas.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 904cdeef4..39c089be9 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -34,7 +34,7 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : - Pretyping.inference_hook option -> + ?inference_hook:Pretyping.inference_hook -> goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit |