diff options
| -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. |