From d206d85fcdea8e825f2bf6b65cebc83263f46803 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Aug 2020 11:36:15 -0700 Subject: [PATCH] fix: trace class name --- src/Lean/Meta/Tactic/Cases.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index a838529734..abcae8cfd4 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -174,10 +174,10 @@ s.mapIdx $ fun i s => { ctorName := ctorNames.get! i, toInductionSubgoal := s } private partial def unifyEqsAux : Nat → CasesSubgoal → MetaM (Option CasesSubgoal) | 0, s => do - trace! `Meta.cases ("unifyEqs " ++ MessageData.ofGoal s.mvarId); + trace! `Meta.Tactic.cases ("unifyEqs " ++ MessageData.ofGoal s.mvarId); pure (some s) | n+1, s => do - trace! `Meta.cases ("unifyEqs [" ++ toString (n+1) ++ "] " ++ MessageData.ofGoal s.mvarId); + trace! `Meta.Tactic.cases ("unifyEqs [" ++ toString (n+1) ++ "] " ++ MessageData.ofGoal s.mvarId); (eqFVarId, mvarId) ← intro1 s.mvarId; withMVarContext mvarId $ do eqDecl ← getLocalDecl eqFVarId; @@ -243,7 +243,7 @@ withMVarContext mvarId $ do pure $ toCasesSubgoals s ctors) (do s₁ ← generalizeIndices mvarId majorFVarId; - trace! `Meta.cases ("after generalizeIndices" ++ Format.line ++ MessageData.ofGoal s₁.mvarId); + trace! `Meta.Tactic.cases ("after generalizeIndices" ++ Format.line ++ MessageData.ofGoal s₁.mvarId); s₂ ← induction s₁.mvarId s₁.fvarId casesOn givenNames useUnusedNames; s₂ ← elimAuxIndices s₁ s₂; let s₂ := toCasesSubgoals s₂ ctors; @@ -254,5 +254,8 @@ end Cases def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) : MetaM (Array CasesSubgoal) := Cases.cases mvarId majorFVarId givenNames useUnusedNames +@[init] private def regTraceClasses : IO Unit := do +registerTraceClass `Meta.Tactic.cases + end Meta end Lean