From 40323e4258d5232226d0be277f53bb5462bac417 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Sep 2019 11:41:28 +0200
Subject: Fix refine and eapply to mark shelved goals as non-resolvable, always

Check that we don't regress on PR #10762 example

Fix regression discovered by Arthur in PR #10762

Fix script of #10298 which was relying on breaking semantics for `eapply`

Add doc

Add comment in clenvtac

Actually, always mark shelved goals as unresolvable

Update doc to reflect semantics w.r.t. shelved subgoals
---
 engine/proofview.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index ed44372045..6f8e668e4e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1025,8 +1025,11 @@ module Unsafe = struct
 
   let undefined = undefined
 
-  let mark_as_unresolvable p gl =
-    { p with solution = mark_in_evm ~goal:false p.solution [gl] }
+  let mark_unresolvables evm evs =
+    mark_in_evm ~goal:false evm evs
+
+  let mark_as_unresolvables p evs =
+    { p with solution = mark_in_evm ~goal:false p.solution evs }
 
 end
 
-- 
cgit v1.2.3