diff options
| author | Matthieu Sozeau | 2016-09-29 14:40:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-29 14:42:42 +0200 |
| commit | 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 (patch) | |
| tree | b75dbe069252890885fe7929aa8614e40b631359 /stm | |
| parent | 875f235dd0413faa34f7d46afc25d2eb90e386e5 (diff) | |
Cleanup API, making inference_hook optional
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 4 | ||||
| -rw-r--r-- | stm/lemmas.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index bf10b91339..022c89ad9a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com use_hook kind thms hook = +let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -460,7 +460,7 @@ let start_proof_com use_hook kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in - let flags = { flags with use_hook } in + let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 904cdeef4d..39c089be9f 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 |