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. --- proofs/pfedit.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e4bae2012..a3ece1913 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -161,11 +161,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in + let ce, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with @@ -232,8 +233,9 @@ let solve_by_implicit_tactic env sigma evk = (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in if Evarutil.has_undefined_evars sigma c then raise Exit; - let (ans, _, _) = + let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in - ans + let sigma = Evd.set_universe_context sigma ctx in + sigma, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit -- cgit v1.2.3