Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvable, always

Reviewed-by: Zimmi48
Reviewed-by: maximedenes

1 files changed, 5 insertions, 2 deletions

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