diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:45:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:47:09 +0200 |
| commit | b46020a6ea52d77b49a12e6891575b3516b8d766 (patch) | |
| tree | bf1fe9bc6d70ac44111f755dca30ed3c4d90b286 /proofs/pfedit.ml | |
| parent | d02c9c566c58e566a1453827038f2b49b695c0a5 (diff) | |
| parent | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 86c2b7a57..c7f5efd5a 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 |