diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Tactics.v | 3 |
1 files changed, 0 insertions, 3 deletions
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 := |