remove logInfo for Branch finishing proof

2024-04-08 12:23:07 +02:00
parent 7cedfc5038
commit ce71bc81c6
1 changed files with 2 additions and 1 deletions
@@ -577,7 +577,8 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
  -- Show an info whether the branch proofs all remaining goals.
  let gs ← Tactic.getUnsolvedGoals
  if gs.isEmpty then
-    trace[debug] "This branch finishes the proof."
+    -- trace[debug] "This branch finishes the proof."
+    pure ()
  else
    trace[debug] "This branch leaves open goals."