diff options
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 | ||||
| -rw-r--r-- | proofs/proofview.ml | 11 |
3 files changed, 18 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35ca18e4f5..b8886b9b54 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1007,6 +1007,9 @@ let principal_future_goal evd = evd.principal_future_goal let reset_future_goals evd = { evd with future_goals = [] ; principal_future_goal=None } +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } + let meta_diff ext orig = Metamap.fold (fun m v acc -> if Metamap.mem m orig then acc diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c15975b0ea..cc64b3594c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -301,6 +301,12 @@ val reset_future_goals : evar_map -> evar_map (** Clears the list of future goals (as well as the principal future goal). Used by the [refine] primitive of the tactic engine. *) +val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map +(** Sets the future goals (including the principal future goal) to a + previous value. Intended to be used after a local list of future + goals has been consumed. Used by the [refine] primitive of the + tactic engine. *) + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given diff --git a/proofs/proofview.ml b/proofs/proofview.ml index cec6f0fad7..50076ed9f3 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1028,10 +1028,15 @@ struct !evdref let refine ?(unsafe = false) f = Goal.enter begin fun gl -> - let sigma = Evd.reset_future_goals (Goal.sigma gl) in + let sigma = Goal.sigma gl in let env = Goal.env gl in let concl = Goal.concl gl in - let (sigma, c) = f sigma in + (** Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.future_goals sigma in + let prev_principal_goal = Evd.principal_future_goal sigma in + (** Create the refinement term *) + let (sigma, c) = f (Evd.reset_future_goals sigma) in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in (** Check that the introduced evars are well-typed *) @@ -1046,6 +1051,8 @@ struct let id = Evd.evar_ident gl.Goal.self sigma in Evd.rename evk id (Evd.define gl.Goal.self c sigma) in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in (** Select the goals *) let comb = undefined sigma (List.rev evs) in let sigma = List.fold_left mark_as_goal sigma comb in |