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.

5 files changed, 24 insertions, 35 deletions

diff --git a/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh b/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
deleted file mode 100644
index c1cb1f15cd..0000000000
--- a/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10760" ] || [ "$CI_BRANCH" = "more-rapply" ]; then
-
-    math_classes_CI_BRANCH=fix-for-more-rapply-10760
-    math_classes_CI_REF=fix-for-more-rapply-10760
-    math_classes_CI_GITURL=https://github.com/JasonGross/math-classes
-
-fi
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`.
diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
index 5bc2322842..13efd986f0 100644
--- a/test-suite/success/rapply.v
+++ b/test-suite/success/rapply.v
@@ -1,22 +1,27 @@
 Require Import Coq.Program.Tactics.
 
+(** We make a version of [rapply] that takes [uconstr]; we do not
+currently test what scope [rapply] interprets terms in. *)
+
+Tactic Notation "urapply" uconstr(p) := rapply p.
+
 Ltac test n :=
   (*let __ := match goal with _ => idtac n end in*)
   lazymatch n with
-  | O => let __ := match goal with _ => assert True by rapply I; clear end in
+  | O => let __ := match goal with _ => assert True by urapply I; clear end in
          uconstr:(fun _ => I)
   | S ?n'
     => let lem := test n' in
-       let __ := match goal with _ => assert True by (unshelve rapply lem; try exact I); clear end in
+       let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in
        uconstr:(fun _ : True => lem)
   end.
 
 Goal True.
-  assert True by rapply I.
-  assert True by (unshelve rapply (fun _ => I); try exact I).
-  assert True by (unshelve rapply (fun _ _ => I); try exact I).
-  assert True by (unshelve rapply (fun _ _ _ => I); try exact I).
+  assert True by urapply I.
+  assert True by (unshelve urapply (fun _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ _ => I); try exact I).
   clear.
   Time let __ := test 50 in idtac.
-  rapply I.
+  urapply I.
 Qed.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 06fc2f73b2..c8a100b0e7 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -178,9 +178,6 @@ Ltac rapply p :=
    rapply uconstr:(p _))
   || refine p.
 
-(** The tactic [rapply] is a tactic notation so that it takes in uconstrs by default *)
-Tactic Notation "rapply" uconstr(p) := rapply p.
-
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 
 Ltac on_call f tac :=