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.

---
 proofs/refine.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/refine.ml')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 50fd1c4722..39d77d983f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -119,7 +119,7 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (** Restore the [future goals] state. *)
-  let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
+  let sigma = Evd.restore_future_goals sigma (prev_future_goals,prev_principal_goal) in
   (** Select the goals *)
   let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
-- 
cgit v1.2.3