diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 6 |
1 files changed, 6 insertions, 0 deletions
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 |