From 29aa2d94b253dad0ade8c877fd7f46b8537a5847 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 21 Feb 2018 23:37:26 +0100
Subject: A comment in Proofview.with_shelf.

---
 engine/proofview.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 53b3cdd9b..22271dd02 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -768,6 +768,8 @@ let with_shelf tac =
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv in
+  (* The pending future goals are necessarily coming from V82.tactic *)
+  (* and thus considered as to shelve, as in Proof.run_tactic *)
   let gls' = Evd.future_goals sigma in
   let fgoals = Evd.save_future_goals solution in
   let sigma = Evd.restore_future_goals sigma fgoals in
-- 
cgit v1.2.3