diff options
| author | Jason Gross | 2019-09-19 16:31:33 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-11-26 14:14:04 -0500 |
| commit | 8d9afb9c459ed7affdf6c0752ff6397e0281e0c3 (patch) | |
| tree | 4f3efc331b48d3068e8e9b340e7ae46db56e4c26 /theories/Program | |
| parent | b09444fdaee1cf608dd40465d5e400fbd46ef6ad (diff) | |
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.
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 := |