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

4 files changed, 7 insertions, 8 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 611671255d..c6a0299cf3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,7 +72,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
         Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
           ~fail:(not with_evars) clenv.env clenv.evd
       in
-      Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
+      (* After an apply, all the subgoals including those dependent shelved ones are in
+         the hands of the user and resolution won't be called implicitely on them. *)
+      Typeclasses.make_unresolvables (fun x -> true) evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2ee006631a..e9f93d0c8f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,12 +386,7 @@ let run_tactic env tac pr =
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
   let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
-  let proofview =
-    List.fold_left
-      Proofview.Unsafe.mark_as_unresolvable
-      proofview
-      to_shelve
-  in
+  let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace),result
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dd8b52e56c..ea42218aaa 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -94,6 +94,7 @@ let generic_refine ~typecheck f gl =
   in
   (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
diff --git a/proofs/refine.mli b/proofs/refine.mli
index bdcccae805..269382489d 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -25,7 +25,8 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand.
+    Shelved evars and goals are all marked as unresolvable for typeclasses. *)
 
 val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic