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 +++++--
 engine/proofview.mli | 9 +++++++--
 2 files changed, 12 insertions(+), 4 deletions(-)

(limited to 'engine')

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
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8ec53ac78c..a92179ab5b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -481,8 +481,13 @@ module Unsafe : sig
       and makes them unresolvable for type classes. *)
   val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
 
-  (** Make an evar unresolvable for type classes. *)
-  val mark_as_unresolvable : proofview -> Evar.t -> proofview
+  (** Make some evars unresolvable for type classes.
+      We need two functions as some functions use the proofview and others
+      directly manipulate the undelying evar_map.
+  *)
+  val mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map
+
+  val mark_as_unresolvables : proofview -> Evar.t list -> proofview
 
   (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
       the current avatar of [g] (for instance [g] was changed by [clear]
-- 
cgit v1.2.3