diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 6 | ||||
| -rw-r--r-- | stm/lemmas.mli | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 5 |
3 files changed, 11 insertions, 4 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 2ab3b9c59..55f33be39 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -451,7 +451,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 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 @@ -461,7 +461,9 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); + let flags = all_and_fail_flags in + let flags = { flags with use_hook = inference_hook } in + evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f0..39c089be9 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : diff --git a/stm/stm.ml b/stm/stm.ml index 3964e6b5c..3fd844f35 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2177,7 +2177,10 @@ let known_state ?(redefine_qed=false) ~cache id = Slaves.build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> reach ~cache:`Shallow start; |