From 8d9afb9c459ed7affdf6c0752ff6397e0281e0c3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 19 Sep 2019 16:31:33 -0400
Subject: 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.
---
 theories/Program/Tactics.v | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'theories/Program')

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 :=
-- 
cgit v1.2.3