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.mli | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'engine/proofview.mli')

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