diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-08 01:47:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-03-08 01:47:40 -0500 |
| commit | 295f86cd4dccaa3a5617f8ac3b4f2dd02b9cfedd (patch) | |
| tree | 6466f73c78ed9b3a680e16f1c67364b244bd6f60 /src/Util | |
| parent | 6b06cc9207e28a531a3241df2760cc8d6427b7fd (diff) | |
Fix grepeat tactic
It previously required progress on all goals, rather than any goal
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Tactics/GlobalTacticals.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tactics/GlobalTacticals.v b/src/Util/Tactics/GlobalTacticals.v index 6c7eac344..8efc56a51 100644 --- a/src/Util/Tactics/GlobalTacticals.v +++ b/src/Util/Tactics/GlobalTacticals.v @@ -4,5 +4,5 @@ Ltac gprogress tac := Tactic Notation "gprogress" tactic3(tac) := gprogress tac. Ltac gtry tac := tac + idtac. Tactic Notation "gtry" tactic3(tac) := gtry tac. -Ltac grepeat tac := gtry (gprogress tac; grepeat tac). +Ltac grepeat tac := gtry (gprogress (gtry tac); grepeat tac). Tactic Notation "grepeat" tactic3(tac) := grepeat tac. |