diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean index 9d7eb5de4..81db87bef 100644 --- a/tests/lean/tactic14.lean +++ b/tests/lean/tactic14.lean @@ -1,7 +1,7 @@ (** -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions -congr_tac = TRY(unfold_tac("eq")) ..REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac)) +congr_tac = TRY(unfold_tac("eq")) .. REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac)) **)