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.

1 files changed, 12 insertions, 7 deletions

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.