From d2c50bb29df8f0b23f7ee498abeda43a672fc688 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 08:58:50 +0100
Subject: Proof engine: consider the pair principal and future goals as an
 entity.

---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 49c953f6d3..49632d2e76 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
-- 
cgit v1.2.3