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.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1a..ea604e08e 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -167,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * + Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> @@ -189,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -(* FIXME: interface: it may incur some new universes etc... *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr -- cgit v1.2.3