diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 49c953f6d..49632d2e7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -303,7 +303,7 @@ 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 +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 |