diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 0ed945f5d4..21cb6f42a7 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,6 +60,10 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) +let map_telescope_evd f = function + | TNil sigma -> TNil (f sigma) + | TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g) + let dependent_init = (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in @@ -74,9 +78,10 @@ let dependent_init = entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> + let t = map_telescope_evd Evd.push_future_goals t in let entry, v = aux t in (* The created goal are not to be shelved. *) - let solution = Evd.reset_future_goals v.solution in + let _goals, solution = Evd.pop_future_goals v.solution in entry, { v with solution } let init = @@ -746,17 +751,16 @@ let with_shelf tac = let open Proof in Pv.get >>= fun pv -> let { shelf; solution } = pv in - Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> + Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >> tac >>= fun ans -> Pv.get >>= fun npv -> let { shelf = gls; solution = sigma } = npv in (* The pending future goals are necessarily coming from V82.tactic *) (* and thus considered as to shelve, as in Proof.run_tactic *) - let gls' = Evd.future_goals sigma in - let fgoals = Evd.save_future_goals solution in - let sigma = Evd.restore_future_goals sigma fgoals in + let fgl, sigma = Evd.pop_future_goals sigma in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined_evars sigma (CList.rev_append gls' gls) in + let gls' = CList.rev_append fgl.Evd.future_shelf (CList.rev_append fgl.Evd.future_comb gls) in + let gls' = undefined_evars sigma gls' in let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -1017,8 +1021,8 @@ module Unsafe = struct let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) - let reset_future_goals p = - { p with solution = Evd.reset_future_goals p.solution } + let push_future_goals p = + { p with solution = Evd.push_future_goals p.solution } let mark_as_goals evd content = mark_in_evm ~goal:true evd content |