diff options
| author | Matthieu Sozeau | 2016-09-28 17:01:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-28 17:02:18 +0200 |
| commit | 875f235dd0413faa34f7d46afc25d2eb90e386e5 (patch) | |
| tree | 9abb3675797e7802bf576a62f0ec6b9f86226465 /proofs | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
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.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 10 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 6 |
2 files changed, 9 insertions, 7 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e4bae20128..a3ece19134 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 diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1af..ea604e08eb 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 |