From 5fa857dc69c945bc1fb74c20e653dccf7bc59667 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Dec 2017 13:47:22 -0800 Subject: [PATCH] fix(library/tactic/tactic_state): do not diplay `case` for empty tag --- src/library/tactic/tactic_state.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 185ebdf7c7..5af8f871e1 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -174,6 +174,7 @@ static format pp_tag(list const & tag) { tmp.push_back(n); } unsigned i = tmp.size(); + if (i == 0) return format(); format r; while (i > 0) { --i;