diff options
| -rw-r--r-- | stm/lemmas.ml | 4 | ||||
| -rw-r--r-- | stm/lemmas.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
3 files changed, 5 insertions, 5 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6723a8b489..f67f6f91ce 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -449,7 +449,7 @@ let vernac_notation locality local = (* Gallina *) let start_proof_and_print k l hook = - let use_hook = + let inference_hook = if Flags.is_program_mode () then let hook env sigma ev = let tac = !Obligations.default_tactic in @@ -468,7 +468,7 @@ let start_proof_and_print k l hook = in Some hook else None in - start_proof_com use_hook k l hook + start_proof_com ?inference_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) |