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

Reviewed-by: Zimmi48
Reviewed-by: maximedenes

2 files changed, 13 insertions, 6 deletions

diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
new file mode 100644
index 0000000000..2fef75dc7f
--- /dev/null
+++ b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  The tactics :tacn:`eapply`, :tacn:`refine` and its variants no
+  longer allows shelved goals to be solved by typeclass resolution.
+  (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 81e50c0834..878118c48a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -555,12 +555,14 @@ Applying theorems
    This tactic applies to any goal. It behaves like :tacn:`exact` with a big
    difference: the user can leave some holes (denoted by ``_``
    or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many
-   subgoals as there are holes in the term. The type of holes must be either
-   synthesized by the system or declared by an explicit cast
+   subgoals as there are remaining holes in the elaborated term. The type
+   of holes must be either synthesized by the system or declared by an explicit cast
    like ``(_ : nat -> Prop)``. Any subgoal that
    occurs in other subgoals is automatically shelved, as if calling
-   :tacn:`shelve_unifiable`. This low-level tactic can be
-   useful to advanced users.
+   :tacn:`shelve_unifiable`. The produced subgoals (shelved or not)
+   are *not* candidates for typeclass resolution, even if they have a type-class
+   type as conclusion, letting the user control when and how typeclass resolution
+   is launched on them. This low-level tactic can be useful to advanced users.
 
    .. example::
 
@@ -611,8 +613,9 @@ Applying theorems
    .. tacv:: simple notypeclasses refine @term
       :name: simple notypeclasses refine
 
-      This tactic behaves like :tacn:`simple refine` except it performs type checking
-      without resolution of typeclasses.
+      This tactic behaves like the combination of :tacn:`simple refine` and
+      :tacn:`notypeclasses refine`: it performs type checking without resolution of
+      typeclasses, does not perform beta reductions or shelve the subgoals.
 
    .. flag:: Debug Unification