From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:01:26 +0200 Subject: Fix bug #4723 and FIXME in API for solve_by_tac This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic. --- stm/lemmas.ml | 6 ++++-- stm/lemmas.mli | 4 +++- 2 files changed, 7 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 50f2b82c3b..bf10b91339 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 kind thms hook = +let start_proof_com use_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 @@ -459,7 +459,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 } 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, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f04..904cdeef4d 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 : + Pretyping.inference_hook option -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : -- cgit v1.2.3 From 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 29 Sep 2016 14:40:00 +0200 Subject: Cleanup API, making inference_hook optional --- stm/lemmas.ml | 4 ++-- stm/lemmas.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') 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 -- cgit v1.2.3 From 89c2942352ec5d8d5b9cfe1116376412770cb396 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 17:33:38 +0200 Subject: STM: compute the correct state for edited Qed (#5086) When a proof is 're-opened', the Qed node does not change. Still the STM has to install the old state (where only the future proof has to be updated). This bit was missing. Why was it working: the bug happens only if you reopen the very last proof, i.e. there is no sentence that stays valid after the Qed. If there is such a sentence, its state was computed correctly before, and is not changed. If it is the very last, then the next state is based on the wrong one... --- stm/stm.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index c53bd958aa..bb4f5f72f3 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; -- cgit v1.2.3