From 295f86cd4dccaa3a5617f8ac3b4f2dd02b9cfedd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 01:47:40 -0500 Subject: Fix grepeat tactic It previously required progress on all goals, rather than any goal --- src/Util/Tactics/GlobalTacticals.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util') 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. -- cgit v1.2.3