From c87e965f861fba4e0e9738ec6252c4181336815e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Dec 2013 21:36:49 -0800 Subject: [PATCH] fix(tests/lean/tactic14.lean): typo Signed-off-by: Leonardo de Moura --- tests/lean/tactic14.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)) **)