Remove `rapply` tactic notation in favor of just the tactic

This increases backwards compatibility.  If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.

2 files changed, 12 insertions, 18 deletions

diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst
index e11a93d654..2815f8af8a 100644
--- a/doc/changelog/04-tactics/10760-more-rapply.rst
+++ b/doc/changelog/04-tactics/10760-more-rapply.rst
@@ -3,17 +3,5 @@
   rare cases where users were relying on :tacn:`rapply` inserting
   exactly 15 underscores and no more, due to the lemma having a
   completely unspecified codomain (and thus allowing for any number of
-  underscores), the tactic will now instead loop.  Additional
-  incompatibility may occur in cases where it was important to
-  interpret the lemma passed in to :tacn:`rapply` as a :g:`constr`
-  (thus failing on unresolved holes and resolving typeclasses before
-  adding arguments) before refining with it.  Users may work around
-  this by replacing all invocations of :tacn:`rapply` with the
-  qualified :g:`Tactics.rapply` to get the underlying tactic rather
-  than the tactic notation.  Finally, any users who defined their own
-  tactic :tacn:`rapply` and also imported :g:`Coq.Program.Tactics` may
-  see incompatibilities due to the fact that :g:`Coq.Program.Tactics`
-  now defines an :tacn:`rapply` as a :cmd:`Tactic Notation`.  Users
-  can work around this by defining their :tacn:`rapply` as a
-  :cmd:`Tactic Notation` as well. (`#10760
+  underscores), the tactic will now instead loop. (`#10760
   <https://github.com/coq/coq/pull/10760>`_, by Jason Gross)
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 843a8933be..3994ff411c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -692,11 +692,17 @@ Applying theorems
       uses the proof engine of :tacn:`refine` for dealing with
       existential variables, holes, and conversion problems.  This may
       result in slightly different behavior regarding which conversion
-      problems are solvable.  Note that :tacn:`rapply` prefers to
-      instantiate as many hypotheses of :n:`@term` as possible.  As a
-      result, if it is possible to apply :n:`@term` to arbitrarily
-      many arguments without getting a type error, :tacn:`rapply` will
-      loop.
+      problems are solvable.  However, like :tacn:`apply` but unlike
+      :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes
+      which remain in :n:`@term` itself after typechecking and
+      typeclass resolution but before unification with the goal.  More
+      technically, :n:`@term` is first parsed as a
+      :production:`constr` rather than as a :production:`uconstr` or
+      :production:`open_constr` before being applied to the goal. Note
+      that :tacn:`rapply` prefers to instantiate as many hypotheses of
+      :n:`@term` as possible.  As a result, if it is possible to apply
+      :n:`@term` to arbitrarily many arguments without getting a type
+      error, :tacn:`rapply` will loop.
 
       Note that you need to :n:`Require Import Coq.Program.Tactics` to
       make use of :tacn:`rapply`.