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/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8a844bbf54..4f8da53787 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -771,7 +771,7 @@ let with_shelf tac =
   let gls' = Evd.future_goals sigma in
   let fgoals = Evd.future_goals solution in
   let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
+  let sigma = Evd.restore_future_goals sigma (fgoals,pgoal) in
   (* Ensure we mark and return only unsolved goals *)
   let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
   let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
-- 
cgit v1.2.3