diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 |
2 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35ca18e4f..b8886b9b5 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 c15975b0e..cc64b3594 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 |